added skomeliation on given type signatures

This commit is contained in:
sebastian 2023-03-28 23:19:04 +02:00
parent 7c5041d270
commit f20b80cab3

View file

@ -66,7 +66,7 @@ preRun (x : xs) = case x of
"Duplicate signatures for function" "Duplicate signatures for function"
quote $ printTree n quote $ printTree n
) )
insertSig (coerce n) (Just t) >> preRun xs insertSig (coerce n) (Just $ skolemize t) >> preRun xs
DBind (Bind n _ e) -> do DBind (Bind n _ e) -> do
collect (collectTVars e) collect (collectTVars e)
s <- gets sigs s <- gets sigs
@ -538,6 +538,12 @@ fresh = do
next 'z' = 'a' next 'z' = 'a'
next a = succ a next a = succ a
skolemize :: Type -> Type
skolemize (TVar (MkTVar a)) = TEVar $ MkTEVar a
skolemize (TAll x t) = TAll x (skolemize t)
skolemize (TFun t1 t2) = (TFun `on` skolemize) t1 t2
skolemize t = t
-- | A class for substitutions -- | A class for substitutions
class SubstType t where class SubstType t where
-- | Apply a substitution to t -- | Apply a substitution to t