diff options
Diffstat (limited to 'src/HSVIS/Typecheck.hs')
| -rw-r--r-- | src/HSVIS/Typecheck.hs | 83 |
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 |