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.hs83
1 files changed, 55 insertions, 28 deletions
diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs
index ba853a0..c97064a 100644
--- a/src/HSVIS/Typecheck.hs
+++ b/src/HSVIS/Typecheck.hs
@@ -78,6 +78,9 @@ type TPattern = Pattern StageTyped
type TRHS = RHS StageTyped
type TExpr = Expr StageTyped
+instance Pretty (E Type StageTC) where
+ prettysPrec _ (TUniVar n) = showString ("?t" ++ show n)
+
instance Pretty (E Kind StageTC) where
prettysPrec _ (KUniVar n) = showString ("?k" ++ show n)
@@ -144,7 +147,7 @@ putFullEnv :: Env -> TCM ()
putFullEnv env = TCM $ \_ i _ -> (mempty, mempty, i, env, ())
genId :: TCM Int
-genId = TCM $ \_ i env -> (mempty, mempty, i, env, i)
+genId = TCM $ \_ i env -> (mempty, mempty, i + 1, env, i)
getKind :: Name -> TCM (Maybe CKind)
getKind name = do
@@ -208,6 +211,8 @@ tcProgram (Program ddefs fdefs) = do
solveKindVars kconstrs
+ traceM (unlines (map pretty ddefs'))
+
fdefs' <- mapM tcFunDef fdefs
return (Program ddefs' fdefs')
@@ -232,40 +237,59 @@ tcDataDef (DataDef rng name params cons) = do
cons' <- scopeTEnv $ do
modifyTEnv (Map.fromList (zip (map snd params) pkinds) <>)
- mapM (\(cname, ty) -> (cname,) <$> mapM kcType ty) cons
+ mapM (\(cname, fieldtys) -> (cname,) <$> mapM (kcType (Just (KType ()))) fieldtys) cons
return (DataDef () name (zip pkinds (map snd params)) cons')
-kcType :: PType -> TCM CType
-kcType = \case
+promoteDown :: Maybe CKind -> TCM CKind
+promoteDown Nothing = genKUniVar
+promoteDown (Just k) = return k
+
+downEqK :: Range -> Maybe CKind -> CKind -> TCM ()
+downEqK _ Nothing _ = return ()
+downEqK rng (Just k1) k2 = emit $ CEqK k1 k2 rng
+
+-- | Given (maybe) the expected kind of this type, and a type, check it for
+-- kind-correctness.
+kcType :: Maybe CKind -> PType -> TCM CType
+kcType mdown = \case
TApp rng t ts -> do
- t' <- kcType t
- ts' <- mapM kcType ts
- retk <- genKUniVar
+ t' <- kcType Nothing t
+ ts' <- mapM (kcType Nothing) ts
+ retk <- promoteDown mdown
let expected = foldr (KFun ()) retk (map extOf ts')
emit $ CEqK (extOf t') expected rng
return (TApp retk t' ts')
- TTup _ ts -> do
- ts' <- mapM kcType ts
+ TTup rng ts -> do
+ ts' <- mapM (kcType (Just (KType ()))) ts
forM_ (zip (map extOf ts) ts') $ \(trng, ct) ->
emit $ CEqK (extOf ct) (KType ()) trng
+ downEqK rng mdown (KType ())
return (TTup (KType ()) ts')
- TList _ t -> do
- t' <- kcType t
+ TList rng t -> do
+ t' <- kcType (Just (KType ())) t
emit $ CEqK (extOf t') (KType ()) (extOf t)
+ downEqK rng mdown (KType ())
return (TList (KType ()) t')
- TFun _ t1 t2 -> do
- t1' <- kcType t1
- t2' <- kcType t2
+ TFun rng t1 t2 -> do
+ t1' <- kcType (Just (KType ())) t1
+ t2' <- kcType (Just (KType ())) t2
emit $ CEqK (extOf t1') (KType ()) (extOf t1)
emit $ CEqK (extOf t2') (KType ()) (extOf t2)
+ downEqK rng mdown (KType ())
return (TFun (KType ()) t1' t2')
- TCon rng n -> TCon <$> getKind' rng n <*> pure n
+ TCon rng n -> do
+ k <- getKind' rng n
+ downEqK rng mdown k
+ return (TCon k n)
- TVar rng n -> TVar <$> getKind' rng n <*> pure n
+ TVar rng n -> do
+ k <- getKind' rng n
+ downEqK rng mdown k
+ return (TVar k n)
tcFunDef :: PFunDef -> TCM CFunDef
tcFunDef (FunDef _ name msig eqs) = do
@@ -273,7 +297,7 @@ tcFunDef (FunDef _ name msig eqs) = do
raise (sconcatne (fmap extOf eqs)) "Function equations have differing numbers of arguments"
typ <- case msig of
- TypeSig sig -> kcType sig
+ TypeSig sig -> kcType (Just (KType ())) sig
TypeSigExt NoTypeSig -> genUniVar (KType ())
eqs' <- mapM (tcFunEq typ) eqs
@@ -326,18 +350,21 @@ solveKindVars cs = do
(\case KExt () (KUniVar v) -> Just v
_ -> Nothing)
kindSize
- (map (\(a, b, _) -> (a, b)) (toList cs))
+ (toList cs)
where
- reduce :: CKind -> CKind -> (Bag (Int, CKind), Bag (CKind, CKind))
- -- unification variables produce constraints on a unification variable
- reduce (KExt () (KUniVar i)) (KExt () (KUniVar j)) | i == j = mempty
- reduce (KExt () (KUniVar i)) k = (pure (i, k), mempty)
- reduce k (KExt () (KUniVar i)) = (pure (i, k), mempty)
- -- if lhs and rhs have equal prefixes, recurse
- reduce (KType ()) (KType ()) = mempty
- reduce (KFun () a b) (KFun () c d) = reduce a c <> reduce b d
- -- otherwise, this is a kind mismatch
- reduce k1 k2 = (mempty, pure (k1, k2))
+ reduce :: CKind -> CKind -> Range -> (Bag (Int, CKind, Range), Bag (CKind, CKind, Range))
+ reduce lhs rhs rng = case (lhs, rhs) of
+ -- unification variables produce constraints on a unification variable
+ (KExt () (KUniVar i), KExt () (KUniVar j)) | i == j -> mempty
+ (KExt () (KUniVar i), k ) -> (pure (i, k, rng), mempty)
+ (k , KExt () (KUniVar i)) -> (pure (i, k, rng), mempty)
+
+ -- if lhs and rhs have equal prefixes, recurse
+ (KType () , KType () ) -> mempty
+ (KFun () a b, KFun () c d) -> reduce a c rng <> reduce b d rng
+
+ -- otherwise, this is a kind mismatch
+ (k1, k2) -> (mempty, pure (k1, k2, rng))
kindSize :: CKind -> Int
kindSize KType{} = 1