diff options
Diffstat (limited to 'src/HSVIS')
| -rw-r--r-- | src/HSVIS/Diagnostic.hs | 2 | ||||
| -rw-r--r-- | src/HSVIS/Pretty.hs | 4 | ||||
| -rw-r--r-- | src/HSVIS/Typecheck.hs | 245 | ||||
| -rw-r--r-- | src/HSVIS/Typecheck/Solve.hs | 22 |
4 files changed, 150 insertions, 123 deletions
diff --git a/src/HSVIS/Diagnostic.hs b/src/HSVIS/Diagnostic.hs index 116e4cd..2794461 100644 --- a/src/HSVIS/Diagnostic.hs +++ b/src/HSVIS/Diagnostic.hs @@ -16,7 +16,7 @@ instance Pretty Pos where -- | Inclusive-exclusive range of positions in a file. data Range = Range Pos Pos - deriving (Show) + deriving (Show, Eq, Ord) instance Semigroup Range where Range a b <> Range c d = Range (min a c) (max b d) diff --git a/src/HSVIS/Pretty.hs b/src/HSVIS/Pretty.hs index cc8cb2a..c25fe08 100644 --- a/src/HSVIS/Pretty.hs +++ b/src/HSVIS/Pretty.hs @@ -9,6 +9,10 @@ class Pretty a where instance Pretty Void where prettysPrec _ = absurd +instance (Pretty a, Pretty b) => Pretty (a, b) where + prettysPrec _ (x, y) = + showString "(" . prettysPrec 0 x . showString ", " . prettysPrec 1 y . showString ")" + prettyPrec :: Pretty a => Int -> a -> String prettyPrec d x = prettysPrec d x "" diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs index 8b642eb..2f68232 100644 --- a/src/HSVIS/Typecheck.hs +++ b/src/HSVIS/Typecheck.hs @@ -19,7 +19,7 @@ module HSVIS.Typecheck ( import Control.Monad import Data.Bifunctor (first, second, bimap) import Data.Foldable (toList) -import Data.List (inits) +import Data.List (inits, foldl1') import Data.Map.Strict (Map) import Data.Maybe (fromMaybe) import qualified Data.Map.Strict as Map @@ -42,13 +42,13 @@ import HSVIS.Typecheck.Solve data StageTC -type instance X DataDef StageTC = CKind +type instance X DataDef StageTC = (Range, CKind) 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 Type StageTC = (Range, CKind) type instance X Pattern StageTC = (Range, CType) type instance X RHS StageTC = CType type instance X Expr StageTC = (Range, CType) @@ -230,8 +230,8 @@ scopeVEnv m = do genKUniVar :: TCM CKind genKUniVar = KExt () . KUniVar <$> genId -genUniVar :: CKind -> TCM CType -genUniVar k = TExt k . TUniVar <$> genId +genUniVar :: Range -> CKind -> TCM CType +genUniVar rng k = TExt (rng, k) . TUniVar <$> genId getKind' :: Range -> Name -> TCM CKind getKind' rng name = getKind name >>= \case @@ -246,7 +246,7 @@ getType' :: Range -> Name -> TCM CType getType' rng name = getType name >>= \case Nothing -> do raise SError rng $ "Variable not in scope: " ++ pretty name - t <- genUniVar (KType ()) -- insert it now so that all occurrences of this out-of-scope name get the same type + t <- genUniVar rng (KType ()) -- insert it now so that all occurrences of this out-of-scope name get the same type modifyVEnv (Map.insert name t) return t Just k -> return k @@ -292,7 +292,7 @@ prepareDataDef (DataDef _ name params _) = do -- Assumes that the kind of the name itself has already been registered with -- the correct arity (this is done by prepareDataDef). kcDataDef :: (CKind, [CKind]) -> PDataDef -> TCM CDataDef -kcDataDef (kd, parkinds) (DataDef _ name params cons) = do +kcDataDef (kd, parkinds) (DataDef defrng name params cons) = do -- ensure unicity of type param names params' <- let prenames = Set.fromList (map snd params) @@ -311,19 +311,23 @@ kcDataDef (kd, parkinds) (DataDef _ name params cons) = do DataField (extOf t) <$> kcType KCTMNormal (Just (KType ())) t return (cname, fields') - return (DataDef kd name (zip parkinds params') cons') + let params_ranges = map fst params + return (DataDef (defrng, kd) name (zip (zip params_ranges parkinds) params') cons') 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) +generateInvCons (DataDef (defrng, k) tname params cons) = + let tyvars = Map.fromList [(n, k1) | ((_rng, k1), n) <- params] + -- defrng is a bit imprecise here, but it's fine + resty = TApp (defrng, KType ()) (TCon (defrng, k) tname) (map (uncurry TVar) params) in [(cname, InvCon tyvars resty (map dataFieldType fields)) | (cname, fields) <- cons] generateConstructors :: CDataDef -> [(Name, CType)] -generateConstructors (DataDef k tname params cons) = - let resty = TApp (KType ()) (TCon k tname) (map (uncurry TVar) params) - in [let funty = foldr (TFun (KType ())) resty (map dataFieldType fields) - in (cname, foldr (\(k1, n1) -> TExt (KType ()) . TForallC (n1, k1)) funty params) +generateConstructors (DataDef (defrng, k) tname params cons) = + -- using defrng is again a bit imprecise here + let resty = TApp (defrng, KType ()) (TCon (defrng, k) tname) (map (uncurry TVar) params) + in [let funty = foldr (TFun (defrng, KType ())) resty (map dataFieldType fields) + in (cname, foldr (\((_, k1), n1) -> TExt (defrng, KType ()) . TForallC (n1, k1)) + funty params) | (cname, fields) <- cons] promoteDownK :: Maybe CKind -> TCM CKind @@ -357,43 +361,45 @@ kcType' mode mdown = \case (ext1, t') <- kcType' mode Nothing t (ext2, ts') <- sequence <$> mapM (kcType' mode Nothing) ts -- TODO: give more useful down kinds retk <- promoteDownK mdown - let expected = foldr (KFun ()) retk (map extOf ts') - emit $ CEqK (extOf t') expected rng - return (ext1 <> ext2, TApp retk t' ts') + let expected = foldr (KFun ()) retk (map (snd . extOf) ts') + emit $ CEqK (snd (extOf t')) expected rng + return (ext1 <> ext2, TApp (rng, retk) t' ts') TTup rng ts -> do (ext, ts') <- sequence <$> mapM (kcType' mode (Just (KType ()))) ts downEqK rng mdown (KType ()) - return (ext, TTup (KType ()) ts') + return (ext, TTup (rng, KType ()) ts') TList rng t -> do (ext, t') <- kcType' mode (Just (KType ())) t downEqK rng mdown (KType ()) - return (ext, TList (KType ()) t') + return (ext, TList (rng, KType ()) t') TFun rng t1 t2 -> do (ext1, t1') <- kcType' mode (Just (KType ())) t1 (ext2, t2') <- kcType' mode (Just (KType ())) t2 downEqK rng mdown (KType ()) - return (ext1 <> ext2, TFun (KType ()) t1' t2') + return (ext1 <> ext2, TFun (rng, KType ()) t1' t2') TCon rng n -> do k <- getKind' rng n downEqK rng mdown k - return (mempty, TCon k n) + return (mempty, TCon (rng, k) n) TVar rng n -> do mk <- getKind n case mk of Nothing -> do k <- promoteDownK mdown - return (case mode of KCTMNormal -> () - KCTMOpen -> MMap.singleton n (pure k) - ,TVar k n) + case mode of + KCTMNormal -> do + raise SError rng $ "Type variable out of scope: " ++ pretty n + return ((), TVar (rng, k) n) + KCTMOpen -> return (MMap.singleton n (pure k), TVar (rng, k) n) Just k -> do downEqK rng mdown k -- TODO: need to instantiate top-level foralls in k here - return (mempty, TVar k n) + return (mempty, TVar (rng, k) n) TExt rng (TForallP n mk1 t) -> do -- implicit forall k1 <- maybe genKUniVar (return . checkKind) mk1 @@ -402,12 +408,13 @@ kcType' mode mdown = \case (ext, t') <- scopeTEnv $ do modifyTEnv (Map.insert n k1) kcType' mode (Just k2) t - return (ext, TExt k2 (TForallC (n, k1) t')) -- 'k2', not 'k1 -> k2', because the forall is implicit + return (ext, TExt (rng, k2) (TForallC (n, k1) t')) -- 'k2', not 'k1 -> k2', because the forall is implicit tcFunDefBlock :: [PFunDef] -> TCM [CFunDef] tcFunDefBlock fdefs = do + let funrange = foldl1' (<>) (map extOf fdefs) -- collect types for each of the bound functions, or unification variables if there's no type signature - bound <- mapM (\(FunDef _ n ts _) -> (n,) <$> tcTypeSig ts) fdefs + bound <- mapM (\(FunDef _ n ts _) -> (n,) <$> tcTypeSig funrange ts) fdefs defs' <- scopeVEnv $ do modifyVEnv (Map.fromList [(n, t) | (n, TypeSig _ t) <- bound] <>) forM (zip fdefs bound) $ \(def, (_, sig)) -> @@ -426,11 +433,15 @@ checkKind :: PKind -> CKind checkKind (KType ()) = KType () checkKind (KFun () k1 k2) = KFun () (checkKind k1) (checkKind k2) -tcTypeSig :: PTypeSig -> TCM CTypeSig -tcTypeSig (TypeSig () sig) = do +-- | The 'Range' argument is the range of the entire function; used in case there +-- is no type signature. +tcTypeSig :: Range -> PTypeSig -> TCM CTypeSig +tcTypeSig _ (TypeSig () sig) = do (typ, freetvars) <- kcType KCTMOpen (Just (KType ())) sig - return $ TypeSig (Just (extOf sig)) $ foldr (\(n, k) -> TExt (KType ()) . TForallC (n, k)) typ (Map.assocs freetvars) -tcTypeSig (TypeSigExt () NoTypeSig) = TypeSig Nothing <$> genUniVar (KType ()) + return $ TypeSig (Just (extOf sig)) $ + foldr (\(n, k) -> TExt (extOf sig, KType ()) . TForallC (n, k)) + typ (Map.assocs freetvars) +tcTypeSig funrange (TypeSigExt () NoTypeSig) = TypeSig Nothing <$> genUniVar funrange (KType ()) -- | Typechecks the function definition, but assumes its signature has already -- been checked, and is passed separately. Thus the PTypeSig in the PFunDef is @@ -468,7 +479,7 @@ tcPattern down = \case PCon rng n ps -> getInvCon n >>= \case Just (InvCon tyvars match fields) -> do - unisub <- mapM genUniVar tyvars -- substitution for the universally quantified variables + unisub <- mapM (genUniVar rng) tyvars -- substitution for the universally quantified variables let match' = substType mempty mempty unisub match fields' = map (substType mempty mempty unisub) fields emit $ CEq down match' rng @@ -480,8 +491,8 @@ tcPattern down = \case POp rng p1 op p2 -> case op of OCons -> do - eltty <- genUniVar (KType ()) - let listty = TList (KType ()) eltty + eltty <- genUniVar rng (KType ()) + let listty = TList (rng, KType ()) eltty emit $ CEq down listty rng p1' <- tcPattern eltty p1 p2' <- tcPattern listty p2 @@ -491,15 +502,16 @@ tcPattern down = \case return (PWildcard (rng, down)) PList rng ps -> do - eltty <- genUniVar (KType ()) - let listty = TList (KType ()) eltty + eltty <- genUniVar rng (KType ()) + let listty = TList (rng, KType ()) eltty emit $ CEq down listty rng PList (rng, listty) <$> mapM (tcPattern eltty) ps PTup rng ps -> do - ts <- mapM (\_ -> genUniVar (KType ())) ps - emit $ CEq down (TTup (KType ()) ts) rng - PTup (rng, TTup (KType ()) ts) <$> zipWithM tcPattern ts ps + ts <- mapM (\p -> genUniVar (extOf p) (KType ())) ps + let typ = TTup (rng, KType ()) ts + emit $ CEq down typ rng + PTup (rng, typ) <$> zipWithM tcPattern ts ps tcRHS :: CType -> PRHS -> TCM CRHS tcRHS _ (Guarded _ _) = error "typecheck: Guards not yet supported" @@ -511,58 +523,61 @@ tcExpr :: CType -> PExpr -> TCM CExpr tcExpr down = \case ELit rng lit -> do let ty = case lit of - LInt{} -> TCon (KType ()) (Name "Int") - LFloat{} -> TCon (KType ()) (Name "Double") - LChar{} -> TCon (KType ()) (Name "Char") - LString{} -> TList (KType ()) (TCon (KType ()) (Name "Char")) + LInt{} -> TCon (rng, KType ()) (Name "Int") + LFloat{} -> TCon (rng, KType ()) (Name "Double") + LChar{} -> TCon (rng, KType ()) (Name "Char") + LString{} -> TList (rng, KType ()) (TCon (rng, KType ()) (Name "Char")) emit $ CEq down ty rng return $ ELit (rng, ty) lit EVar rng n -> do ty <- getType' rng n - ty' <- instantiateTForallsUni ty + ty' <- instantiateTForallsUni rng ty emit $ CEq down ty' rng return $ EVar (rng, ty') n ECon rng n -> do ty <- getType' rng n - ty' <- instantiateTForallsUni ty + ty' <- instantiateTForallsUni rng ty emit $ CEq down ty' rng return $ EVar (rng, ty') n EList rng es -> do - eltty <- genUniVar (KType ()) - let listty = TList (KType ()) eltty + eltty <- genUniVar rng (KType ()) + let listty = TList (rng, KType ()) eltty emit $ CEq down listty rng EList (rng, listty) <$> mapM (tcExpr listty) es ETup rng es -> do - ts <- mapM (\_ -> genUniVar (KType ())) es - emit $ CEq down (TTup (KType ()) ts) rng - ETup (rng, TTup (KType ()) ts) <$> zipWithM tcExpr ts es + ts <- mapM (\_ -> genUniVar rng (KType ())) es + let typ = TTup (rng, KType ()) ts + emit $ CEq down typ rng + ETup (rng, typ) <$> zipWithM tcExpr ts es EApp rng e1 es -> do - argtys <- mapM (\_ -> genUniVar (KType ())) es - let funty = foldr (TFun (KType ())) down argtys + argtys <- mapM (\e -> genUniVar (extOf e) (KType ())) es + let funty = foldr (TFun (rng, KType ())) down argtys 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 EOp rng e1 op e2 -> do - let int = TCon (KType ()) (Name "Int") - bool = TCon (KType ()) (Name "Bool") + let int = \r -> TCon (r, KType ()) (Name "Int") + bool = \r -> TCon (r, KType ()) (Name "Bool") + rng1 = extOf e1 + rng2 = extOf e2 (rty, aty1, aty2) <- case op of - OAdd -> return (int, int, int) - OSub -> return (int, int, int) - OMul -> return (int, int, int) - ODiv -> return (int, int, int) - OMod -> return (int, int, int) - OEqu -> return (bool, int, int) - OPow -> return (int, int, int) + OAdd -> return (int rng, int rng1, int rng2) + OSub -> return (int rng, int rng1, int rng2) + OMul -> return (int rng, int rng1, int rng2) + ODiv -> return (int rng, int rng1, int rng2) + OMod -> return (int rng, int rng1, int rng2) + OEqu -> return (bool rng, int rng1, int rng2) + OPow -> return (int rng, int rng1, int rng2) OCons -> do - eltty <- genUniVar (KType ()) - let listty = TList (KType ()) eltty + eltty <- genUniVar rng1 (KType ()) + let listty = TList (rng2, KType ()) eltty return (listty, eltty, listty) emit $ CEq down rty rng e1' <- tcExpr aty1 e1 @@ -570,13 +585,13 @@ tcExpr down = \case return (EOp (rng, rty) e1' op e2') EIf rng e1 e2 e3 -> do - e1' <- tcExpr (TCon (KType ()) (Name "Bool")) e1 + e1' <- tcExpr (TCon (rng, KType ()) (Name "Bool")) e1 e2' <- tcExpr down e2 e3' <- tcExpr down e3 return (EIf (rng, down) e1' e2' e3') ECase rng e1 alts -> do - ty <- genUniVar (KType ()) + ty <- genUniVar rng (KType ()) e1' <- tcExpr ty e1 alts' <- forM alts $ \(pat, rhs) -> scopeVEnv $ @@ -593,11 +608,12 @@ tcExpr down = \case EError rng -> return $ EError (rng, down) -instantiateTForallsUni :: CType -> TCM CType -instantiateTForallsUni = go mempty +-- | The 'Range' is the place where the type is being instantiated. +instantiateTForallsUni :: Range -> CType -> TCM CType +instantiateTForallsUni instRng = go mempty where go sub (TExt _ (TForallC (n, k1) t)) = do - var <- genUniVar k1 + var <- genUniVar instRng k1 go (Map.insert n var sub) t go sub t = return $ substType mempty mempty sub t @@ -607,9 +623,9 @@ unfoldFunTy rng n (TFun _ t1 t2) = do (params, core) <- unfoldFunTy rng (n - 1) t2 return (t1 : params, core) unfoldFunTy rng n t = do - vars <- replicateM n (genUniVar (KType ())) - core <- genUniVar (KType ()) - let expected = foldr (TFun (KType ())) core vars + vars <- replicateM n (genUniVar rng (KType ())) + core <- genUniVar rng (KType ()) + let expected = foldr (TFun (rng, KType ())) core vars emit $ CEq expected t rng return (vars, core) @@ -708,8 +724,8 @@ solveTypeVars cs = do (TCon _ n1, TCon _ n2) | n1 == n2 -> mempty (TVar _ n1, TVar _ n2) | n1 == n2 -> mempty -- TODO: this doesn't check that the types are kind-correct. Did we already check that? - (TExt _ (TForallC (n1, k) t1), TExt _ (TForallC (n2, _) t2)) -> - reduce t1 (substType mempty mempty (Map.singleton n2 (TVar k n1)) t2) rng + (TExt (rng1, _) (TForallC (n1, k) t1), TExt _ (TForallC (n2, _) t2)) -> + reduce t1 (substType mempty mempty (Map.singleton n2 (TVar (rng1, k) n1)) t2) rng -- otherwise, this is a kind mismatch (k1, k2) -> (mempty, pure (k1, k2, rng)) @@ -738,9 +754,9 @@ 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 :: 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) +substDdef mk mt (DataDef (defrng, k) name pars cons) = + DataDef (defrng, substKind mk k) name + (map (first (second (substKind mk))) pars) (map (second (map (substDataField mk mt))) cons) substDataField :: Map Int CKind -> Map Int CType -> CDataField -> CDataField @@ -795,14 +811,14 @@ substExpr mk mt = go 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) - go (TTup k ts) = TTup (goKind k) (map go ts) - go (TList k t) = TList (goKind k) (go t) - go (TFun k t1 t2) = TFun (goKind k) (go t1) (go t2) - go (TCon k n) = TCon (goKind k) n - go (TVar k n) = fromMaybe (TVar (goKind k) n) (Map.lookup n mtv) - go (TExt k (TUniVar v)) = fromMaybe (TExt (goKind k) (TUniVar v)) (Map.lookup v mt) - go (TExt k (TForallC (n, k1) t)) = TExt (goKind k) (TForallC (n, goKind k1) (go t)) + go (TApp (rng, k) t ts) = TApp (rng, goKind k) (go t) (map go ts) + go (TTup (rng, k) ts) = TTup (rng, goKind k) (map go ts) + go (TList (rng, k) t) = TList (rng, goKind k) (go t) + go (TFun (rng, k) t1 t2) = TFun (rng, goKind k) (go t1) (go t2) + go (TCon (rng, k) n) = TCon (rng, goKind k) n + go (TVar (rng, k) n) = fromMaybe (TVar (rng, goKind k) n) (Map.lookup n mtv) + go (TExt (rng, k) (TUniVar v)) = fromMaybe (TExt (rng, goKind k) (TUniVar v)) (Map.lookup v mt) + go (TExt (rng, k) (TForallC (n, k1) t)) = TExt (rng, goKind k) (TForallC (n, goKind k1) (go t)) goKind = substKind mk @@ -820,18 +836,18 @@ 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 +finaliseDdef (DataDef (rng, k) name pars cons) = + DataDef <$> finaliseKind rng k <*> pure name + <*> traverse (firstM (finaliseKind rng . snd)) pars <*> traverse (secondM (traverse finaliseDataField)) cons finaliseDataField :: MonadRaise m => CDataField -> m TDataField -finaliseDataField (DataField rng t) = DataField rng <$> finaliseType rng t +finaliseDataField (DataField rng t) = DataField rng <$> finaliseType t finaliseFdef :: MonadRaise m => CFunDef -> m TFunDef -finaliseFdef (FunDef rng n (TypeSig msigrng sig) eqs) = +finaliseFdef (FunDef _ n (TypeSig _ sig) eqs) = FunDef () n - <$> (TypeSig () <$> finaliseType (fromMaybe rng msigrng) sig) + <$> (TypeSig () <$> finaliseType sig) <*> traverse finaliseFunEq eqs finaliseFunEq :: MonadRaise m => CFunEq -> m TFunEq @@ -842,7 +858,7 @@ finaliseFunEq (FunEq () n ps 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 +finaliseRHS (Plain t e) = Plain <$> finaliseType t <*> finaliseExpr e finalisePattern :: MonadRaise m => CPattern -> m TPattern finalisePattern = \case @@ -854,7 +870,7 @@ finalisePattern = \case 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 + goExt (_, t) = finaliseType t finaliseExpr :: MonadRaise m => CExpr -> m TExpr finaliseExpr = \case @@ -870,28 +886,35 @@ finaliseExpr = \case ELet e defs body -> ELet <$> goExt e <*> traverse finaliseFdef defs <*> finaliseExpr body EError e -> EError <$> goExt e where - goExt (rng, t) = finaliseType rng t + goExt (_, t) = finaliseType t -finaliseType :: MonadRaise m => Range -> CType -> m TType -finaliseType rng toptype = go toptype +finaliseType :: MonadRaise m => CType -> m TType +finaliseType toptype = go toptype where - go :: MonadRaise m => Type StageTC -> m TType - 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 t@(TExt k TUniVar{}) = do + go :: MonadRaise m => CType -> m TType + go (TApp e t ts) = TApp <$> goExt e <*> go t <*> traverse go ts + go (TTup e ts) = TTup <$> goExt e <*> traverse go ts + go (TList e t) = TList <$> goExt e <*> go t + go (TFun e t1 t2) = TFun <$> goExt e <*> go t1 <*> go t2 + go (TCon e n) = TCon <$> goExt e <*> pure n + go (TVar e n) = TVar <$> goExt e <*> pure n + go t@(TExt (rng, k) TUniVar{}) = do raise SError rng $ "Ambiguous type unification variable " ++ pretty t ++ " in type: " ++ pretty toptype - TVar <$> finaliseKind k <*> pure (Name "$_error") - go (TExt k (TForallC (n, k1) t)) = TExt <$> finaliseKind k <*> (TForall <$> ((,) <$> pure n <*> finaliseKind k1) <*> go t) + TVar <$> finaliseKind rng k <*> pure (Name "$_error") + go (TExt e@(rng, _) (TForallC (n, k1) t)) = + TExt <$> goExt e <*> (TForall <$> ((n,) <$> finaliseKind rng k1) <*> go t) -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 + goExt (rng, t) = finaliseKind rng t + +finaliseKind :: MonadRaise m => Range -> CKind -> m TKind +finaliseKind toprng topkind = go topkind + where + go :: MonadRaise m => CKind -> m TKind + go (KType ()) = pure (KType ()) + go (KFun () k1 k2) = KFun () <$> go k1 <*> go k2 + go k@(KExt () KUniVar{}) = do + raise SError toprng $ "Ambiguous kind unification variable " ++ pretty k ++ " in kind: " ++ pretty topkind + pure $ KType () -------------------- END OF FINALISATION FUNCTIONS -------------------- diff --git a/src/HSVIS/Typecheck/Solve.hs b/src/HSVIS/Typecheck/Solve.hs index 250d7e7..7b91585 100644 --- a/src/HSVIS/Typecheck/Solve.hs +++ b/src/HSVIS/Typecheck/Solve.hs @@ -84,7 +84,7 @@ solveConstraints reduce frees subst detect size = \tupcs -> in trace ("[solver] Solving:" ++ concat ["\n- " ++ pretty a ++ " == " ++ pretty b ++ " {" ++ pretty r ++ "}" | Constr a b r <- cs]) $ trace ("[solver] Result: (with " ++ show (length errs'') ++ " errors)" ++ concat ["\n- " ++ show v ++ " = " ++ pretty t | (v, t) <- Map.assocs asg'] ++ - "\n... errors: " ++ intercalate ", " (map summariseUE (toList errs''))) + "\n... errors: [" ++ intercalate ", " (map summariseUE (toList errs'')) ++ "]") (asg', errs'') where reduce' :: Constr t t -> (Bag (Constr v t), Bag (Constr t t)) @@ -92,14 +92,14 @@ solveConstraints reduce frees subst detect size = \tupcs -> loop :: Map v (Bag (RConstr t)) -> [(v, t)] -> (Bag (UnifyErr v t), Map v t) loop m eqlog = do - traceM $ "[solver] Step:" ++ concat - [case toList rhss of - [] -> "\n- " ++ show v ++ " <no RHSs>" - RConstr t r : rest -> - "\n- " ++ show v ++ " == " ++ pretty t ++ " {" ++ pretty r ++ "}" ++ - concat ["\n " ++ replicate (length (show v)) ' ' ++ " == " ++ pretty t' ++ " {" ++ pretty r' ++ "}" - | RConstr t' r' <- rest] - | (v, rhss) <- Map.assocs m] + -- traceM $ "[solver] Step:" ++ concat + -- [case toList rhss of + -- [] -> "\n- " ++ show v ++ " <no RHSs>" + -- RConstr t r : rest -> + -- "\n- " ++ show v ++ " == " ++ pretty t ++ " {" ++ pretty r ++ "}" ++ + -- concat ["\n " ++ replicate (length (show v)) ' ' ++ " == " ++ pretty t' ++ " {" ++ pretty r' ++ "}" + -- | RConstr t' r' <- rest] + -- | (v, rhss) <- Map.assocs m] m' <- Map.traverseWithKey (\v rhss -> @@ -120,10 +120,10 @@ solveConstraints reduce frees subst detect size = \tupcs -> case msmallestvar of Nothing -> do - traceM $ "[solver] Log = [" ++ intercalate ", " [show v ++ " = " ++ pretty t | (v, t) <- eqlog] ++ "]" + -- traceM $ "[solver] Log = [" ++ intercalate ", " [show v ++ " = " ++ pretty t | (v, t) <- eqlog] ++ "]" return $ applyLog eqlog mempty Just (var, RConstr smallrhs _) -> do - traceM $ "[solver] Retiring " ++ show var ++ " = " ++ pretty smallrhs + -- traceM $ "[solver] Retiring " ++ show var ++ " = " ++ pretty smallrhs let (_, otherrhss) = bagPartition (guard . (== smallrhs) . rconType) (m' Map.! var) let (newcs, errs) = foldMap (reduce' . unsplitConstr smallrhs) (dedupRCs (toList otherrhss)) (fmap constrUnequal errs, ()) -- write the errors |