aboutsummaryrefslogtreecommitdiff
path: root/src/HSVIS/Typecheck.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/HSVIS/Typecheck.hs')
-rw-r--r--src/HSVIS/Typecheck.hs292
1 files changed, 186 insertions, 106 deletions
diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs
index 2dd103f..1e46a99 100644
--- a/src/HSVIS/Typecheck.hs
+++ b/src/HSVIS/Typecheck.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
@@ -7,40 +8,28 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE GADTs #-}
-
-
-
-{-# OPTIONS -Wno-unused-top-binds #-}
-{-# OPTIONS -Wno-unused-imports #-}
-{-# LANGUAGE DataKinds #-}
-
-
-
module HSVIS.Typecheck (
StageTyped,
typecheck,
-- * Typed AST synonyms
- -- TProgram, TDataDef, TFunDef, TFunEq, TKind, TType, TPattern, TRHS, TExpr,
+ TProgram, TDataDef, TDataField, TFunDef, TFunEq, TKind, TType, TPattern, TRHS, TExpr,
) where
import Control.Monad
import Data.Bifunctor (first, second, bimap)
import Data.Foldable (toList)
-import Data.List (find, inits)
+import Data.List (inits)
import Data.Map.Strict (Map)
import Data.Maybe (fromMaybe)
-import Data.Monoid (Ap(..))
import qualified Data.Map.Strict as Map
import Data.Tuple (swap)
import Data.Semigroup (First(..))
import Data.Set (Set)
import qualified Data.Set as Set
-import GHC.Stack
import Debug.Trace
import Data.Bag
-import Data.List.NonEmpty.Util
import Data.Map.Monoidal (MMap(..))
import qualified Data.Map.Monoidal as MMap
import HSVIS.AST
@@ -53,13 +42,15 @@ import HSVIS.Typecheck.Solve
data StageTC
type instance X DataDef StageTC = CKind
-type instance X FunDef StageTC = CType
+type instance X DataField StageTC = Range
+type instance X FunDef StageTC = Range
+type instance X TypeSig StageTC = Maybe Range
type instance X FunEq StageTC = ()
type instance X Kind StageTC = ()
type instance X Type StageTC = CKind
-type instance X Pattern StageTC = CType
+type instance X Pattern StageTC = (Range, CType)
type instance X RHS StageTC = CType
-type instance X Expr StageTC = CType
+type instance X Expr StageTC = (Range, CType)
data instance E Type StageTC = TUniVar Int deriving (Show, Eq, Ord)
data instance E Kind StageTC = KUniVar Int deriving (Show, Eq, Ord)
@@ -67,6 +58,7 @@ data instance E TypeSig StageTC deriving (Show)
type CProgram = Program StageTC
type CDataDef = DataDef StageTC
+type CDataField = DataField StageTC
type CFunDef = FunDef StageTC
type CFunEq = FunEq StageTC
type CKind = Kind StageTC
@@ -78,7 +70,9 @@ type CExpr = Expr StageTC
data StageTyped
type instance X DataDef StageTyped = TKind
-type instance X FunDef StageTyped = TType
+type instance X DataField StageTyped = Range
+type instance X FunDef StageTyped = ()
+type instance X TypeSig StageTyped = ()
type instance X FunEq StageTyped = ()
type instance X Kind StageTyped = ()
type instance X Type StageTyped = TKind
@@ -92,6 +86,7 @@ data instance E TypeSig StageTyped deriving (Show)
type TProgram = Program StageTyped
type TDataDef = DataDef StageTyped
+type TDataField = DataField StageTyped
type TFunDef = FunDef StageTyped
type TFunEq = FunEq StageTyped
type TKind = Kind StageTyped
@@ -251,7 +246,7 @@ tcTop :: PProgram -> TCM TProgram
tcTop prog = do
(cs, prog') <- collectConstraints Just (tcProgram prog)
(subK, subT) <- solveConstrs cs
- return $ finaliseProg (substProg subK subT prog')
+ finaliseProg (substProg subK subT prog')
tcProgram :: PProgram -> TCM CProgram
tcProgram (Program ddefs1 fdefs1) = do
@@ -301,9 +296,10 @@ kcDataDef (kd, parkinds) (DataDef _ name params cons) = do
-- kind-check the constructors
cons' <- scopeTEnv $ do
modifyTEnv (Map.fromList (zip params' parkinds) <>)
- forM cons $ \(cname, fieldtys) -> do
- fieldtys' <- mapM (kcType KCTMNormal (Just (KType ()))) fieldtys
- return (cname, fieldtys')
+ forM cons $ \(cname, fields) -> do
+ fields' <- forM fields $ \(DataField () t) ->
+ DataField (extOf t) <$> kcType KCTMNormal (Just (KType ())) t
+ return (cname, fields')
return (DataDef kd name (zip parkinds params') cons')
@@ -311,7 +307,7 @@ generateInvCons :: CDataDef -> [(Name, InvCon)]
generateInvCons (DataDef k tname params cons) =
let tyvars = Map.fromList (map swap params)
resty = TApp (KType ()) (TCon k tname) (map (uncurry TVar) params)
- in [(cname, InvCon tyvars resty fields) | (cname, fields) <- cons]
+ in [(cname, InvCon tyvars resty (map dataFieldType fields)) | (cname, fields) <- cons]
promoteDownK :: Maybe CKind -> TCM CKind
promoteDownK Nothing = genKUniVar
@@ -401,7 +397,7 @@ tcFunDefBlock fdefs = do
-- take the actual found types for typechecking the body (and link them
-- to the variables generated above)
- let bound2 = map (\(FunDef ty n _ _) -> (n, ty)) defs'
+ let bound2 = map (\(FunDef _ n (TypeSig _ ty) _) -> (n, ty)) defs'
forM_ (zip3 fdefs bound bound2) $ \(fdef, (_, tvar), (_, ty)) ->
emit $ CEq ty tvar (extOf fdef) -- which is expected/observed? which range? /shrug/
@@ -412,8 +408,8 @@ tcFunDef (FunDef rng name msig eqs) = do
when (not $ allEq (fmap (length . funeqPats) eqs)) $
raise SError rng "Function equations have differing numbers of arguments"
- typ <- case msig of
- TypeSig sig -> do
+ (typ, msigrng) <- case msig of
+ TypeSig _ sig -> do
(typ, freetvars) <- kcType KCTMOpen (Just (KType ())) sig
TODO -- We need to check that these free type variables do not escape.
-- Perhaps with levels on unification variables? Associate a level
@@ -421,14 +417,15 @@ tcFunDef (FunDef rng name msig eqs) = do
-- passing below a forall.
-- But how do we deal with functions without a type signature
-- anyway? We should be able to infer a polymorphic type for them.
- return $ foldr (\(n, k) -> TForall k n) typ (Map.assocs freetvars)
- TypeSigExt NoTypeSig -> genUniVar (KType ())
+ return (foldr (\(n, k) -> TForall k n) typ (Map.assocs freetvars)
+ ,Just (extOf sig))
+ TypeSigExt _ NoTypeSig -> (,Nothing) <$> genUniVar (KType ())
eqs' <- scopeVEnv $ do
modifyVEnv (Map.insert name typ) -- allow function to be recursive
mapM (tcFunEq typ) eqs
- return (FunDef typ name (TypeSig typ) eqs')
+ return (FunDef rng name (TypeSig msigrng typ) eqs')
tcFunEq :: CType -> PFunEq -> TCM CFunEq
tcFunEq down (FunEq rng name pats rhs) = do
@@ -442,11 +439,14 @@ tcFunEq down (FunEq rng name pats rhs) = do
-- | Brings the bound variables in scope
tcPattern :: CType -> PPattern -> TCM CPattern
tcPattern down = \case
- PWildcard _ -> return $ PWildcard down
+ PWildcard rng -> return $ PWildcard (rng, down)
- PVar _ n -> modifyVEnv (Map.insert n down) >> return (PVar down n)
+ PVar rng n -> modifyVEnv (Map.insert n down) >> return (PVar (rng, down) n)
- PAs _ n p -> modifyVEnv (Map.insert n down) >> tcPattern down p
+ PAs rng n p -> do
+ modifyVEnv (Map.insert n down)
+ p' <- tcPattern down p
+ return $ PAs (rng, snd (extOf p')) n p'
PCon rng n ps ->
getInvCon n >>= \case
@@ -455,10 +455,10 @@ tcPattern down = \case
let match' = substType mempty mempty unisub match
fields' = map (substType mempty mempty unisub) fields
emit $ CEq down match' rng
- PCon match' n <$> zipWithM tcPattern fields' ps
+ PCon (rng, match') n <$> zipWithM tcPattern fields' ps
Nothing -> do
raise SError rng $ "Constructor not in scope: " ++ pretty n
- return (PWildcard down)
+ return (PWildcard (rng, down))
POp rng p1 op p2 ->
case op of
@@ -468,27 +468,27 @@ tcPattern down = \case
emit $ CEq down listty rng
p1' <- tcPattern eltty p1
p2' <- tcPattern listty p2
- return (POp listty p1' OCons p2')
+ return (POp (rng, listty) p1' OCons p2')
_ -> do
raise SError rng $ "Operator is not a constructor: " ++ pretty op
- return (PWildcard down)
+ return (PWildcard (rng, down))
PList rng ps -> do
eltty <- genUniVar (KType ())
let listty = TList (KType ()) eltty
emit $ CEq down listty rng
- PList listty <$> mapM (tcPattern eltty) ps
+ PList (rng, listty) <$> mapM (tcPattern eltty) ps
PTup rng ps -> do
ts <- mapM (\_ -> genUniVar (KType ())) ps
emit $ CEq down (TTup (KType ()) ts) rng
- PTup (TTup (KType ()) ts) <$> zipWithM tcPattern ts ps
+ PTup (rng, TTup (KType ()) ts) <$> zipWithM tcPattern ts ps
tcRHS :: CType -> PRHS -> TCM CRHS
tcRHS _ (Guarded _ _) = error "typecheck: Guards not yet supported"
tcRHS down (Plain _ e) = do
e' <- tcExpr down e
- return $ Plain (extOf e') e'
+ return $ Plain (snd (extOf e')) e'
tcExpr :: CType -> PExpr -> TCM CExpr
tcExpr down = \case
@@ -499,34 +499,34 @@ tcExpr down = \case
LChar{} -> TCon (KType ()) (Name "Char")
LString{} -> TList (KType ()) (TCon (KType ()) (Name "Char"))
emit $ CEq down ty rng
- return (ELit ty lit)
+ return $ ELit (rng, ty) lit
EVar rng n -> do
ty <- getType' rng n
emit $ CEq down ty rng
- return $ EVar ty n
+ return $ EVar (rng, ty) n
ECon rng n -> do
ty <- getType' rng n
emit $ CEq down ty rng
- return $ EVar ty n
+ return $ EVar (rng, ty) n
EList rng es -> do
eltty <- genUniVar (KType ())
let listty = TList (KType ()) eltty
emit $ CEq down listty rng
- EList listty <$> mapM (tcExpr listty) es
+ EList (rng, listty) <$> mapM (tcExpr listty) es
ETup rng es -> do
ts <- mapM (\_ -> genUniVar (KType ())) es
emit $ CEq down (TTup (KType ()) ts) rng
- ETup (TTup (KType ()) ts) <$> zipWithM tcExpr ts es
+ ETup (rng, TTup (KType ()) ts) <$> zipWithM tcExpr ts es
- EApp _ e1 es -> do
+ EApp rng e1 es -> do
argtys <- mapM (\_ -> genUniVar (KType ())) es
let funty = foldr (TFun (KType ())) down argtys
- EApp funty <$> tcExpr funty e1
- <*> zipWithM tcExpr argtys es
+ EApp (rng, funty) <$> tcExpr funty e1
+ <*> zipWithM tcExpr argtys es
-- TODO: these types are way too monomorphic and in any case these
-- ~operators~ functions should not be built-in
@@ -548,31 +548,31 @@ tcExpr down = \case
emit $ CEq down rty rng
e1' <- tcExpr aty1 e1
e2' <- tcExpr aty2 e2
- return (EOp rty e1' op e2')
+ return (EOp (rng, rty) e1' op e2')
- EIf _ e1 e2 e3 -> do
+ EIf rng e1 e2 e3 -> do
e1' <- tcExpr (TCon (KType ()) (Name "Bool")) e1
e2' <- tcExpr down e2
e3' <- tcExpr down e3
- return (EIf down e1' e2' e3')
+ return (EIf (rng, down) e1' e2' e3')
- ECase _ e1 alts -> do
+ ECase rng e1 alts -> do
ty <- genUniVar (KType ())
e1' <- tcExpr ty e1
alts' <- forM alts $ \(pat, rhs) ->
scopeVEnv $
(,) <$> tcPattern ty pat <*> tcRHS down rhs
- return $ ECase down e1' alts'
+ return $ ECase (rng, down) e1' alts'
- ELet _ defs body -> do
+ ELet rng defs body -> do
defs' <- tcFunDefBlock defs
- let bound2 = map (\(FunDef ty n _ _) -> (n, ty)) defs'
+ let bound2 = map (\(FunDef _ n (TypeSig _ ty) _) -> (n, ty)) defs'
scopeVEnv $ do
modifyVEnv (Map.fromList bound2 <>)
body' <- tcExpr down body
- return $ ELet down defs' body'
+ return $ ELet (rng, down) defs' body'
- EError _ -> return $ EError down
+ EError rng -> return $ EError (rng, down)
unfoldFunTy :: Range -> Int -> CType -> TCM ([CType], CType)
unfoldFunTy _ n t | n <= 0 = return ([], t)
@@ -706,70 +706,65 @@ partitionConstrs = foldMap $ \case CEq t1 t2 r -> (pure (t1, t2, r), mempty)
-- - an instantiation map for type unification variables (Map Int CType)
-- - an instantiation map for type variables (Map Name CType)
-substProg :: HasCallStack
- => Map Int CKind -> Map Int CType -> CProgram -> CProgram
+substProg :: Map Int CKind -> Map Int CType -> CProgram -> CProgram
substProg mk mt (Program ds fs) = Program (map (substDdef mk mt) ds) (map (substFdef mk mt) fs)
-substDdef :: HasCallStack
- => Map Int CKind -> Map Int CType -> CDataDef -> CDataDef
+substDdef :: Map Int CKind -> Map Int CType -> CDataDef -> CDataDef
substDdef mk mt (DataDef k name pars cons) =
DataDef (substKind mk k) name
(map (first (substKind mk)) pars)
- (map (second (map (substType mk mt mempty))) cons)
+ (map (second (map (substDataField mk mt))) cons)
+
+substDataField :: Map Int CKind -> Map Int CType -> CDataField -> CDataField
+substDataField mk mt (DataField rng t) = DataField rng (substType mk mt mempty t)
-substFdef :: HasCallStack
- => Map Int CKind -> Map Int CType -> CFunDef -> CFunDef
-substFdef mk mt (FunDef t n (TypeSig sig) eqs) =
- FunDef (substType mk mt mempty t) n
- (TypeSig (substType mk mt mempty sig))
+substFdef :: Map Int CKind -> Map Int CType -> CFunDef -> CFunDef
+substFdef mk mt (FunDef rng n (TypeSig sigrng sig) eqs) =
+ FunDef rng n
+ (TypeSig sigrng (substType mk mt mempty sig))
(fmap (substFunEq mk mt) eqs)
-substFunEq :: HasCallStack
- => Map Int CKind -> Map Int CType -> CFunEq -> CFunEq
+substFunEq :: Map Int CKind -> Map Int CType -> CFunEq -> CFunEq
substFunEq mk mt (FunEq () n ps rhs) =
FunEq () n
(map (substPattern mk mt) ps)
(substRHS mk mt rhs)
-substRHS :: HasCallStack
- => Map Int CKind -> Map Int CType -> CRHS -> CRHS
+substRHS :: Map Int CKind -> Map Int CType -> CRHS -> CRHS
substRHS _ _ (Guarded _ _) = error "typecheck: guards unsupported"
substRHS mk mt (Plain t e) = Plain (substType mk mt mempty t) (substExpr mk mt e)
-substPattern :: HasCallStack
- => Map Int CKind -> Map Int CType -> CPattern -> CPattern
+substPattern :: Map Int CKind -> Map Int CType -> CPattern -> CPattern
substPattern mk mt = go
where
- go (PWildcard t) = PWildcard (goType t)
- go (PVar t n) = PVar (goType t) n
- go (PAs t n p) = PAs (goType t) n (go p)
- go (PCon t n ps) = PCon (goType t) n (map go ps)
- go (POp t p1 op p2) = POp (goType t) (go p1) op (go p2)
- go (PList t ps) = PList (goType t) (map go ps)
- go (PTup t ps) = PTup (goType t) (map go ps)
-
- goType = substType mk mt mempty
-
-substExpr :: HasCallStack
- => Map Int CKind -> Map Int CType -> CExpr -> CExpr
+ go (PWildcard e) = PWildcard (goExt e)
+ go (PVar e n) = PVar (goExt e) n
+ go (PAs e n p) = PAs (goExt e) n (go p)
+ go (PCon e n ps) = PCon (goExt e) n (map go ps)
+ go (POp e p1 op p2) = POp (goExt e) (go p1) op (go p2)
+ go (PList e ps) = PList (goExt e) (map go ps)
+ go (PTup e ps) = PTup (goExt e) (map go ps)
+
+ goExt (rng, t) = (rng, substType mk mt mempty t)
+
+substExpr :: Map Int CKind -> Map Int CType -> CExpr -> CExpr
substExpr mk mt = go
where
- go (ELit t lit) = ELit (goType t) lit
- go (EVar t n) = EVar (goType t) n
- go (ECon t n) = ECon (goType t) n
- go (EList t es) = EList (goType t) (map go es)
- go (ETup t es) = ETup (goType t) (map go es)
- go (EApp t e1 es) = EApp (goType t) (go e1) (map go es)
- go (EOp t e1 op e2) = EOp (goType t) (go e1) op (go e2)
- go (EIf t e1 e2 e3) = EIf (goType t) (go e1) (go e2) (go e3)
- go (ECase t e1 alts) = ECase (goType t) (go e1) (map (bimap (substPattern mk mt) (substRHS mk mt)) alts)
- go (ELet t defs body) = ELet (goType t) (map (substFdef mk mt) defs) (go body)
- go (EError t) = EError (goType t)
-
- goType = substType mk mt mempty
-
-substType :: HasCallStack
- => Map Int CKind -> Map Int CType -> Map Name CType -> CType -> CType
+ go (ELit e lit) = ELit (goExt e) lit
+ go (EVar e n) = EVar (goExt e) n
+ go (ECon e n) = ECon (goExt e) n
+ go (EList e es) = EList (goExt e) (map go es)
+ go (ETup e es) = ETup (goExt e) (map go es)
+ go (EApp e e1 es) = EApp (goExt e) (go e1) (map go es)
+ go (EOp e e1 op e2) = EOp (goExt e) (go e1) op (go e2)
+ go (EIf e e1 e2 e3) = EIf (goExt e) (go e1) (go e2) (go e3)
+ go (ECase e e1 alts) = ECase (goExt e) (go e1) (map (bimap (substPattern mk mt) (substRHS mk mt)) alts)
+ go (ELet e defs body) = ELet (goExt e) (map (substFdef mk mt) defs) (go body)
+ go (EError e) = EError (goExt e)
+
+ goExt (rng, t) = (rng, substType mk mt mempty t)
+
+substType :: Map Int CKind -> Map Int CType -> Map Name CType -> CType -> CType
substType mk mt mtv = go
where
go (TApp k t ts) = TApp (goKind k) (go t) (map go ts)
@@ -783,8 +778,7 @@ substType mk mt mtv = go
goKind = substKind mk
-substKind :: HasCallStack
- => Map Int CKind -> CKind -> CKind
+substKind :: Map Int CKind -> CKind -> CKind
substKind m = \case
KType () -> KType ()
KFun () k1 k2 -> KFun () (substKind m k1) (substKind m k2)
@@ -793,7 +787,84 @@ substKind m = \case
-------------------- FINALISATION FUNCTIONS --------------------
-- These report free type unification variables.
--- TODO the finalise* functions
+finaliseProg :: MonadRaise m => CProgram -> m TProgram
+finaliseProg (Program ds fs) =
+ Program <$> traverse finaliseDdef ds <*> traverse finaliseFdef fs
+
+finaliseDdef :: MonadRaise m => CDataDef -> m TDataDef
+finaliseDdef (DataDef k name pars cons) =
+ DataDef <$> finaliseKind k <*> pure name
+ <*> traverse (firstM finaliseKind) pars
+ <*> traverse (secondM (traverse finaliseDataField)) cons
+
+finaliseDataField :: MonadRaise m => CDataField -> m TDataField
+finaliseDataField (DataField rng t) = DataField rng <$> finaliseType rng t
+
+finaliseFdef :: MonadRaise m => CFunDef -> m TFunDef
+finaliseFdef (FunDef rng n (TypeSig msigrng sig) eqs) =
+ FunDef () n
+ <$> (TypeSig () <$> finaliseType (fromMaybe rng msigrng) sig)
+ <*> traverse finaliseFunEq eqs
+
+finaliseFunEq :: MonadRaise m => CFunEq -> m TFunEq
+finaliseFunEq (FunEq () n ps rhs) =
+ FunEq () n
+ <$> traverse finalisePattern ps
+ <*> finaliseRHS rhs
+
+finaliseRHS :: MonadRaise m => CRHS -> m TRHS
+finaliseRHS (Guarded _ _) = error "typecheck: guards unsupported"
+finaliseRHS (Plain t e) = Plain <$> finaliseType (fst (extOf e)) t <*> finaliseExpr e
+
+finalisePattern :: MonadRaise m => CPattern -> m TPattern
+finalisePattern = \case
+ PWildcard e -> PWildcard <$> goExt e
+ PVar e n -> PVar <$> goExt e <*> pure n
+ PAs e n p -> PAs <$> goExt e <*> pure n <*> finalisePattern p
+ PCon e n ps -> PCon <$> goExt e <*> pure n <*> traverse finalisePattern ps
+ POp e p1 op p2 -> POp <$> goExt e <*> finalisePattern p1 <*> pure op <*> finalisePattern p2
+ PList e ps -> PList <$> goExt e <*> traverse finalisePattern ps
+ PTup e ps -> PTup <$> goExt e <*> traverse finalisePattern ps
+ where
+ goExt (rng, t) = finaliseType rng t
+
+finaliseExpr :: MonadRaise m => CExpr -> m TExpr
+finaliseExpr = \case
+ ELit e lit -> ELit <$> goExt e <*> pure lit
+ EVar e n -> EVar <$> goExt e <*> pure n
+ ECon e n -> ECon <$> goExt e <*> pure n
+ EList e es -> EList <$> goExt e <*> traverse finaliseExpr es
+ ETup e es -> ETup <$> goExt e <*> traverse finaliseExpr es
+ EApp e e1 es -> EApp <$> goExt e <*> finaliseExpr e1 <*> traverse finaliseExpr es
+ EOp e e1 op e2 -> EOp <$> goExt e <*> finaliseExpr e1 <*> pure op <*> finaliseExpr e2
+ EIf e e1 e2 e3 -> EIf <$> goExt e <*> finaliseExpr e1 <*> finaliseExpr e2 <*> finaliseExpr e3
+ ECase e e1 alts -> ECase <$> goExt e <*> finaliseExpr e1 <*> traverse (bimapM finalisePattern finaliseRHS) alts
+ ELet e defs body -> ELet <$> goExt e <*> traverse finaliseFdef defs <*> finaliseExpr body
+ EError e -> EError <$> goExt e
+ where
+ goExt (rng, t) = finaliseType rng t
+
+finaliseType :: MonadRaise m => Range -> CType -> m TType
+finaliseType rng toptype = go toptype
+ where
+ go (TApp k t ts) = TApp <$> finaliseKind k <*> go t <*> traverse go ts
+ go (TTup k ts) = TTup <$> finaliseKind k <*> traverse go ts
+ go (TList k t) = TList <$> finaliseKind k <*> go t
+ go (TFun k t1 t2) = TFun <$> finaliseKind k <*> go t1 <*> go t2
+ go (TCon k n) = TCon <$> finaliseKind k <*> pure n
+ go (TVar k n) = TVar <$> finaliseKind k <*> pure n
+ go (TForall k n t) = TForall <$> finaliseKind k <*> pure n <*> go t
+ go t@(TExt k TUniVar{}) = do
+ raise SError rng $ "Ambiguous type unification variable " ++ pretty t ++ " in type: " ++ pretty toptype
+ TVar <$> finaliseKind k <*> pure (Name "$_error")
+
+finaliseKind :: MonadRaise m => CKind -> m TKind
+finaliseKind = \case
+ KType () -> pure (KType ())
+ KFun () k1 k2 -> KFun () <$> finaliseKind k1 <*> finaliseKind k2
+ k@(KExt () KUniVar{}) -> error $ "Unresolved kind variable: " ++ pretty k
+
+-------------------- END OF FINALISATION FUNCTIONS --------------------
typeUniVars :: CType -> Set Int
typeUniVars = \case
@@ -817,12 +888,21 @@ allEq l = case toList l of
[] -> True
x : xs -> all (== x) xs
-funeqPats :: FunEq t -> [Pattern t]
+funeqPats :: FunEq s -> [Pattern s]
funeqPats (FunEq _ _ pats _) = pats
+dataFieldType :: DataField s -> Type s
+dataFieldType (DataField _ t) = t
+
isCEqK :: Constr -> Maybe (CKind, CKind, Range)
isCEqK (CEqK k1 k2 rng) = Just (k1, k2, rng)
isCEqK _ = Nothing
-foldMapM :: (Applicative f, Monoid m, Foldable t) => (a -> f m) -> t a -> f m
-foldMapM f = getAp . foldMap (Ap . f)
+firstM :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
+firstM f (x, y) = (,y) <$> f x
+
+secondM :: Functor f => (b -> f c) -> (a, b) -> f (a, c)
+secondM f (x, y) = (x,) <$> f y
+
+bimapM :: Applicative f => (a -> f b) -> (c -> f d) -> (a, c) -> f (b, d)
+bimapM f g (x, y) = (,) <$> f x <*> g y
generated by cgit v1.2.3-70-g09d2 (git 2.47.0) at 2024-11-01 06:34:02 +0100