aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/tc.hs10
-rw-r--r--examples/test-kinds.hs2
-rw-r--r--src/HSVIS/AST.hs8
-rw-r--r--src/HSVIS/Parser.hs10
-rw-r--r--src/HSVIS/Pretty.hs3
-rw-r--r--src/HSVIS/Typecheck.hs167
-rw-r--r--src/HSVIS/Typecheck/Solve.hs8
7 files changed, 129 insertions, 79 deletions
diff --git a/examples/tc.hs b/examples/tc.hs
new file mode 100644
index 0000000..c27c736
--- /dev/null
+++ b/examples/tc.hs
@@ -0,0 +1,10 @@
+data Bool = False | True
+data List a = Nil | Cons a (List a)
+
+isNil :: List a -> Bool
+isNil Nil = True
+isNil (Cons _ _) = False
+
+map :: (a -> b) -> List a -> List b
+map _ Nil = Nil
+map f (Cons x l) = Cons (f x) (map f l)
diff --git a/examples/test-kinds.hs b/examples/test-kinds.hs
index 1e2c18c..ddd4817 100644
--- a/examples/test-kinds.hs
+++ b/examples/test-kinds.hs
@@ -8,6 +8,8 @@ data Either a b = Left a | Right b
data ExceptT e m a = ExceptT (Either e (m a))
+data ExceptT2 e m a = ExceptT2 (m (Either e a))
+
data TreeF a r
= NodeF r a r
| LeafF
diff --git a/src/HSVIS/AST.hs b/src/HSVIS/AST.hs
index 63594bc..6c0b323 100644
--- a/src/HSVIS/AST.hs
+++ b/src/HSVIS/AST.hs
@@ -98,7 +98,7 @@ data Type s
| TFun (X Type s) (Type s) (Type s)
| TCon (X Type s) Name
| TVar (X Type s) Name
- | TForall (X Type s) Name (Type s) -- ^ implicit; also, not parsed
+ -- | TForall (X Type s) Name (Type s) -- ^ implicit; also, not parsed
-- extension point
| TExt (X Type s) !(E Type s)
@@ -163,8 +163,8 @@ instance Pretty (E Type s) => Pretty (Type s) where
prettysPrec 0 a . showString " -> " . prettysPrec (-1) b
prettysPrec _ (TCon _ n) = prettysPrec 11 n
prettysPrec _ (TVar _ n) = prettysPrec 11 n
- prettysPrec d (TForall _ n t) = showParen (d > -1) $
- showString "forall " . prettysPrec 11 n . showString ". " . prettysPrec (-1) t
+ -- prettysPrec d (TForall _ n t) = showParen (d > -1) $
+ -- showString "forall " . prettysPrec 11 n . showString ". " . prettysPrec (-1) t
prettysPrec d (TExt _ e) = prettysPrec d e
instance (Pretty (X Type s), Pretty (E Type s)) => Pretty (DataDef s) where
@@ -254,7 +254,7 @@ instance HasExt Type where
extOf (TFun x _ _) = x
extOf (TCon x _) = x
extOf (TVar x _) = x
- extOf (TForall x _ _) = x
+ -- extOf (TForall x _ _) = x
extOf (TExt x _) = x
-- extMap p ps1 ps2 f g (TApp x a b) = TApp (f x) (extMap p ps1 ps2 f g a) (map (extMap p ps1 ps2 f g) b)
diff --git a/src/HSVIS/Parser.hs b/src/HSVIS/Parser.hs
index 0d35184..2110ca1 100644
--- a/src/HSVIS/Parser.hs
+++ b/src/HSVIS/Parser.hs
@@ -20,8 +20,8 @@ module HSVIS.Parser (
StageParsed,
parse,
-- * Staged AST synonyms
- PProgram, PDataDef, PFunDef, PFunEq, PType, PPattern, PRHS, PExpr,
- E(NoTypeSig),
+ PProgram, PDataDef, PFunDef, PTypeSig, PFunEq, PKind, PType, PPattern, PRHS, PExpr,
+ E(NoTypeSig, TForallP),
) where
-- import Control.Applicative
@@ -54,20 +54,22 @@ type instance X DataField StageParsed = ()
type instance X FunDef StageParsed = Range
type instance X TypeSig StageParsed = ()
type instance X FunEq StageParsed = Range
+type instance X Kind StageParsed = ()
type instance X Type StageParsed = Range
type instance X Pattern StageParsed = Range
type instance X RHS StageParsed = Range
type instance X Expr StageParsed = Range
data instance E TypeSig StageParsed = NoTypeSig deriving (Show)
-data instance E Type StageParsed deriving (Show)
+data instance E Type StageParsed = TForallP Name (Maybe PKind) PType deriving (Show)
data instance E Kind StageParsed deriving (Show)
type PProgram = Program StageParsed
type PDataDef = DataDef StageParsed
type PFunDef = FunDef StageParsed
--- type PTypeSig = TypeSig StageParsed
+type PTypeSig = TypeSig StageParsed
type PFunEq = FunEq StageParsed
+type PKind = Kind StageParsed
type PType = Type StageParsed
type PPattern = Pattern StageParsed
type PRHS = RHS StageParsed
diff --git a/src/HSVIS/Pretty.hs b/src/HSVIS/Pretty.hs
index 0f98da3..cc8cb2a 100644
--- a/src/HSVIS/Pretty.hs
+++ b/src/HSVIS/Pretty.hs
@@ -12,5 +12,8 @@ instance Pretty Void where
prettyPrec :: Pretty a => Int -> a -> String
prettyPrec d x = prettysPrec d x ""
+prettys :: Pretty a => a -> ShowS
+prettys = prettysPrec 0
+
pretty :: Pretty a => a -> String
pretty x = prettyPrec minBound x
diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs
index 1e46a99..8b642eb 100644
--- a/src/HSVIS/Typecheck.hs
+++ b/src/HSVIS/Typecheck.hs
@@ -1,13 +1,14 @@
+{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
module HSVIS.Typecheck (
StageTyped,
typecheck,
@@ -52,7 +53,7 @@ type instance X Pattern StageTC = (Range, CType)
type instance X RHS StageTC = CType
type instance X Expr StageTC = (Range, CType)
-data instance E Type StageTC = TUniVar Int deriving (Show, Eq, Ord)
+data instance E Type StageTC = TUniVar Int | TForallC (Name, CKind) CType deriving (Show, Eq, Ord)
data instance E Kind StageTC = KUniVar Int deriving (Show, Eq, Ord)
data instance E TypeSig StageTC deriving (Show)
@@ -60,6 +61,7 @@ type CProgram = Program StageTC
type CDataDef = DataDef StageTC
type CDataField = DataField StageTC
type CFunDef = FunDef StageTC
+type CTypeSig = TypeSig StageTC
type CFunEq = FunEq StageTC
type CKind = Kind StageTC
type CType = Type StageTC
@@ -80,7 +82,7 @@ type instance X Pattern StageTyped = TType
type instance X RHS StageTyped = TType
type instance X Expr StageTyped = TType
-data instance E Type StageTyped deriving (Show)
+data instance E Type StageTyped = TForall (Name, TKind) TType deriving (Show)
data instance E Kind StageTyped deriving (Show)
data instance E TypeSig StageTyped deriving (Show)
@@ -97,6 +99,8 @@ type TExpr = Expr StageTyped
instance Pretty (E Type StageTC) where
prettysPrec _ (TUniVar n) = showString ("?t" ++ show n)
+ prettysPrec d (TForallC (n, k) t) = showParen (d > 0) $
+ showString "forall (" . prettys n . showString " :: " . prettys k . showString "). " . prettys t
instance Pretty (E Kind StageTC) where
prettysPrec _ (KUniVar n) = showString ("?k" ++ show n)
@@ -140,17 +144,18 @@ newtype TCM a = TCM {
instance Functor TCM where
fmap f (TCM g) = TCM $ \ctx i env ->
- let (ds, cs, i', env', x) = g ctx i env
- in (ds, cs, i', env', f x)
+ let !(ds, cs, i', env', !x) = g ctx i env
+ !res = f x
+ in (ds, cs, i', env', res)
instance Applicative TCM where
- pure x = TCM $ \_ i env -> (mempty, mempty, i, env, x)
+ pure x = TCM $ \_ i env -> x `seq` (mempty, mempty, i, env, x)
(<*>) = ap
instance Monad TCM where
TCM f >>= g = TCM $ \ctx i1 env1 ->
- let (ds2, cs2, i2, env2, x) = f ctx i1 env1
- (ds3, cs3, i3, env3, y) = runTCM (g x) ctx i2 env2
+ let !(ds2, cs2, i2, env2, !x) = f ctx i1 env1
+ !(ds3, cs3, i3, env3, !y) = runTCM (g x) ctx i2 env2
in (ds2 <> ds3, cs2 <> cs3, i3, env3, y)
class Monad m => MonadRaise m where
@@ -232,14 +237,18 @@ getKind' :: Range -> Name -> TCM CKind
getKind' rng name = getKind name >>= \case
Nothing -> do
raise SError rng $ "Type not in scope: " ++ pretty name
- genKUniVar
+ k <- genKUniVar -- insert it now so that all occurrences of this out-of-scope name get the same kind
+ modifyTEnv (Map.insert name k)
+ return k
Just k -> return k
getType' :: Range -> Name -> TCM CType
getType' rng name = getType name >>= \case
Nothing -> do
raise SError rng $ "Variable not in scope: " ++ pretty name
- genUniVar (KType ())
+ t <- genUniVar (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
tcTop :: PProgram -> TCM TProgram
@@ -260,8 +269,9 @@ tcProgram (Program ddefs1 fdefs1) = do
let ddefs3 = map (substDdef kinduvars mempty) ddefs2
modifyTEnv (Map.map (substKind kinduvars))
- -- generate inverse constructors for all data types
- forM_ ddefs3 $ \ddef ->
+ -- generate constructor values and inverse constructors for all data types
+ forM_ ddefs3 $ \ddef -> do
+ modifyVEnv (Map.fromList (generateConstructors ddef) <>)
modifyICEnv (Map.fromList (generateInvCons ddef) <>)
traceM (unlines (map pretty ddefs3))
@@ -309,6 +319,13 @@ generateInvCons (DataDef k tname params cons) =
resty = TApp (KType ()) (TCon 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)
+ | (cname, fields) <- cons]
+
promoteDownK :: Maybe CKind -> TCM CKind
promoteDownK Nothing = genKUniVar
promoteDownK (Just k) = return k
@@ -338,7 +355,7 @@ kcType' :: forall ext ret. Monoid ext => KCTypeMode ext ret -> Maybe CKind -> PT
kcType' mode mdown = \case
TApp rng t ts -> do
(ext1, t') <- kcType' mode Nothing t
- (ext2, ts') <- sequence <$> mapM (kcType' mode Nothing) ts
+ (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
@@ -346,22 +363,17 @@ kcType' mode mdown = \case
TTup rng ts -> do
(ext, ts') <- sequence <$> mapM (kcType' mode (Just (KType ()))) ts
- forM_ (zip (map extOf ts) ts') $ \(trng, ct) ->
- emit $ CEqK (extOf ct) (KType ()) trng
downEqK rng mdown (KType ())
return (ext, TTup (KType ()) ts')
TList rng t -> do
(ext, t') <- kcType' mode (Just (KType ())) t
- emit $ CEqK (extOf t') (KType ()) (extOf t)
downEqK rng mdown (KType ())
return (ext, TList (KType ()) t')
TFun rng t1 t2 -> do
(ext1, t1') <- kcType' mode (Just (KType ())) t1
(ext2, t2') <- kcType' mode (Just (KType ())) t2
- emit $ CEqK (extOf t1') (KType ()) (extOf t1)
- emit $ CEqK (extOf t2') (KType ()) (extOf t2)
downEqK rng mdown (KType ())
return (ext1 <> ext2, TFun (KType ()) t1' t2')
@@ -371,61 +383,66 @@ kcType' mode mdown = \case
return (mempty, TCon k n)
TVar rng n -> do
- k <- getKind' rng n
- downEqK rng mdown k
- return (case mode of KCTMNormal -> ()
- KCTMOpen -> MMap.singleton n (pure k)
- ,TVar k n)
-
- TForall rng n t -> do -- implicit forall
- k1 <- genKUniVar
+ 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)
+ Just k -> do
+ downEqK rng mdown k
+ -- TODO: need to instantiate top-level foralls in k here
+ return (mempty, TVar k n)
+
+ TExt rng (TForallP n mk1 t) -> do -- implicit forall
+ k1 <- maybe genKUniVar (return . checkKind) mk1
k2 <- genKUniVar
downEqK rng mdown k2
(ext, t') <- scopeTEnv $ do
modifyTEnv (Map.insert n k1)
kcType' mode (Just k2) t
- return (ext, TForall k2 n t') -- not 'k1 -> k2' because the forall is implicit
+ return (ext, TExt k2 (TForallC (n, k1) t')) -- 'k2', not 'k1 -> k2', because the forall is implicit
tcFunDefBlock :: [PFunDef] -> TCM [CFunDef]
tcFunDefBlock fdefs = do
- -- generate preliminary unification variables for the functions' types
- bound <- mapM (\(FunDef _ n _ _) -> (n,) <$> genUniVar (KType ())) fdefs
- defs' <- forM fdefs $ \def@(FunDef _ name _ _) ->
- scopeVEnv $ do
- modifyVEnv (Map.fromList [(n, t) | (n, t) <- bound, n /= name] <>)
- tcFunDef def
-
- -- take the actual found types for typechecking the body (and link them
- -- to the variables generated above)
- 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/
+ -- 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
+ defs' <- scopeVEnv $ do
+ modifyVEnv (Map.fromList [(n, t) | (n, TypeSig _ t) <- bound] <>)
+ forM (zip fdefs bound) $ \(def, (_, sig)) ->
+ tcFunDef sig def
+
+ -- -- take the actual found types for typechecking the body (and link them
+ -- -- to the variables generated above)
+ -- 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/
return defs'
-tcFunDef :: PFunDef -> TCM CFunDef
-tcFunDef (FunDef rng name msig eqs) = do
+-- | Just the identity, because there's nothing to be checked in our simple kinds
+checkKind :: PKind -> CKind
+checkKind (KType ()) = KType ()
+checkKind (KFun () k1 k2) = KFun () (checkKind k1) (checkKind k2)
+
+tcTypeSig :: 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 ())
+
+-- | Typechecks the function definition, but assumes its signature has already
+-- been checked, and is passed separately. Thus the PTypeSig in the PFunDef is
+-- ignored.
+tcFunDef :: CTypeSig -> PFunDef -> TCM CFunDef
+tcFunDef typesig@(TypeSig _ funtyp) (FunDef rng name _ eqs) = do
when (not $ allEq (fmap (length . funeqPats) eqs)) $
raise SError rng "Function equations have differing numbers of arguments"
- (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
- -- to a generated uvar, and increment the global level counter when
- -- 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)
- ,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 rng name (TypeSig msigrng typ) eqs')
+ eqs' <- scopeVEnv $ mapM (tcFunEq funtyp) eqs
+
+ return (FunDef rng name typesig eqs')
tcFunEq :: CType -> PFunEq -> TCM CFunEq
tcFunEq down (FunEq rng name pats rhs) = do
@@ -503,13 +520,15 @@ tcExpr down = \case
EVar rng n -> do
ty <- getType' rng n
- emit $ CEq down ty rng
- return $ EVar (rng, ty) n
+ ty' <- instantiateTForallsUni ty
+ emit $ CEq down ty' rng
+ return $ EVar (rng, ty') n
ECon rng n -> do
ty <- getType' rng n
- emit $ CEq down ty rng
- return $ EVar (rng, ty) n
+ ty' <- instantiateTForallsUni ty
+ emit $ CEq down ty' rng
+ return $ EVar (rng, ty') n
EList rng es -> do
eltty <- genUniVar (KType ())
@@ -574,6 +593,14 @@ tcExpr down = \case
EError rng -> return $ EError (rng, down)
+instantiateTForallsUni :: CType -> TCM CType
+instantiateTForallsUni = go mempty
+ where
+ go sub (TExt _ (TForallC (n, k1) t)) = do
+ var <- genUniVar k1
+ go (Map.insert n var sub) t
+ go sub t = return $ substType mempty mempty sub t
+
unfoldFunTy :: Range -> Int -> CType -> TCM ([CType], CType)
unfoldFunTy _ n t | n <= 0 = return ([], t)
unfoldFunTy rng n (TFun _ t1 t2) = do
@@ -680,7 +707,8 @@ solveTypeVars cs = do
(TFun _ t1 t2, TFun _ t1' t2') -> reduce t1 t1' rng <> reduce t2 t2' rng
(TCon _ n1, TCon _ n2) | n1 == n2 -> mempty
(TVar _ n1, TVar _ n2) | n1 == n2 -> mempty
- (TForall _ n1 t1, TForall k n2 t2) ->
+ -- 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
-- otherwise, this is a kind mismatch
@@ -693,8 +721,8 @@ solveTypeVars cs = do
typeSize (TFun _ t1 t2) = typeSize t1 + typeSize t2
typeSize (TCon _ _) = 1
typeSize (TVar _ _) = 1
- typeSize (TForall _ _ t) = 1 + typeSize t
typeSize (TExt _ TUniVar{}) = 2
+ typeSize (TExt _ (TForallC _ t)) = 1 + typeSize t
partitionConstrs :: Foldable t => t Constr -> (Bag (CType, CType, Range), Bag (CKind, CKind, Range))
partitionConstrs = foldMap $ \case CEq t1 t2 r -> (pure (t1, t2, r), mempty)
@@ -773,8 +801,8 @@ substType mk mt mtv = go
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 (TForall k n t) = TForall (goKind k) n (go t)
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))
goKind = substKind mk
@@ -847,16 +875,17 @@ finaliseExpr = \case
finaliseType :: MonadRaise m => Range -> CType -> m TType
finaliseType rng 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 (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")
+ go (TExt k (TForallC (n, k1) t)) = TExt <$> finaliseKind k <*> (TForall <$> ((,) <$> pure n <*> finaliseKind k1) <*> go t)
finaliseKind :: MonadRaise m => CKind -> m TKind
finaliseKind = \case
@@ -874,8 +903,8 @@ typeUniVars = \case
TFun _ t1 t2 -> typeUniVars t1 <> typeUniVars t2
TCon _ _ -> mempty
TVar _ _ -> mempty
- TForall _ _ t -> typeUniVars t
TExt _ (TUniVar v) -> Set.singleton v
+ TExt _ (TForallC _ t) -> typeUniVars t
kindUniVars :: CKind -> Set Int
kindUniVars = \case
diff --git a/src/HSVIS/Typecheck/Solve.hs b/src/HSVIS/Typecheck/Solve.hs
index 7250e79..250d7e7 100644
--- a/src/HSVIS/Typecheck/Solve.hs
+++ b/src/HSVIS/Typecheck/Solve.hs
@@ -83,7 +83,8 @@ solveConstraints reduce frees subst detect size = \tupcs ->
errs'' = fmap constrUnequal errs <> errs'
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'])
+ concat ["\n- " ++ show v ++ " = " ++ pretty t | (v, t) <- Map.assocs asg'] ++
+ "\n... errors: " ++ intercalate ", " (map summariseUE (toList errs'')))
(asg', errs'')
where
reduce' :: Constr t t -> (Bag (Constr v t), Bag (Constr t t))
@@ -136,10 +137,13 @@ solveConstraints reduce frees subst detect size = \tupcs ->
applyLog ((v, t) : l) m = applyLog l $ Map.insert v (subst m t) m
applyLog [] m = m
- -- If there are multiple sources for the same cosntraint, only one of them is kept.
+ -- If there are multiple sources for the same constraint, only one of them is kept.
dedupRCs :: Ord t => [RConstr t] -> [RConstr t]
dedupRCs = map head . groupBy ((==) `on` rconType) . sortBy (comparing rconType)
+ summariseUE (UEUnequal t1 t2 rng) = "({" ++ pretty rng ++ "} " ++ pretty t1 ++ " /= " ++ pretty t2 ++ ")"
+ summariseUE (UERecursive v t2 rng) = "({" ++ pretty rng ++ "} [" ++ show v ++ "] rec in " ++ pretty t2 ++ ")"
+
minimumByMay :: Foldable t' => (a -> a -> Ordering) -> t' a -> Maybe a
minimumByMay cmp = foldl' min' Nothing
where min' mx y = Just $! case mx of
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-03-10 08:52:36 +0100