git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Mutually recursive data types, part 2
2992586Phil Freeman
examples/passing/MutRec.purs−2
compare with golang
unifiedsplit
@@ -9,9 +9,7 @@ module MutRec where
9
9
10 data Odd = Odd Even
10 data Odd = Odd Even
11
11
12− evenToNumber :: Even -> Number
13 evenToNumber Zero = 0
12 evenToNumber Zero = 0
14 evenToNumber (Even n) = oddToNumber n + 1
13 evenToNumber (Even n) = oddToNumber n + 1
15
14
16− oddToNumber :: Odd -> Number
17 oddToNumber (Odd n) = evenToNumber n + 1
15 oddToNumber (Odd n) = evenToNumber n + 1
src/Language/PureScript/TypeChecker.hs+73−36
@@ -35,53 +35,90 @@ import Language.PureScript.Names
35import Language.PureScript.Kinds
35import Language.PureScript.Kinds
36import Language.PureScript.Declarations
36import Language.PureScript.Declarations
37
37
38+addDataType :: ModuleName -> ProperName -> [String] -> [(ProperName, Maybe Type)] -> Kind -> Check ()
39+addDataType moduleName name args dctors ctorKind = do
40+ env <- getEnv
41+ putEnv $ env { types = M.insert (moduleName, name) (ctorKind, Data) (types env) }
42+ forM_ dctors $ \(dctor, maybeTy) ->
43+ rethrow (("Error in data constructor " ++ show name ++ ":\n") ++) $
44+ addDataConstructor moduleName name args dctor maybeTy
45+
46+addDataConstructor :: ModuleName -> ProperName -> [String] -> ProperName -> Maybe Type -> Check ()
47+addDataConstructor moduleName name args dctor maybeTy = do
48+ env <- getEnv
49+ dataConstructorIsNotDefined moduleName dctor
50+ let retTy = foldl TypeApp (TypeConstructor (Qualified (Just moduleName) name)) (map TypeVar args)
51+ let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy
52+ let polyType = mkForAll args dctorTy
53+ putEnv $ env { dataConstructors = M.insert (moduleName, dctor) polyType (dataConstructors env) }
54+
55+addTypeSynonym :: ModuleName -> ProperName -> [String] -> Type -> Kind -> Check ()
56+addTypeSynonym moduleName name args ty kind = do
57+ env <- getEnv
58+ putEnv $ env { types = M.insert (moduleName, name) (kind, TypeSynonym) (types env)
59+ , typeSynonyms = M.insert (moduleName, name) (args, ty) (typeSynonyms env) }
60+
61+typeIsNotDefined :: ModuleName -> ProperName -> Check ()
62+typeIsNotDefined moduleName name = do
63+ env <- getEnv
64+ guardWith (show name ++ " is already defined") $
65+ not $ M.member (moduleName, name) (types env)
66+
67+dataConstructorIsNotDefined :: ModuleName -> ProperName -> Check ()
68+dataConstructorIsNotDefined moduleName dctor = do
69+ env <- getEnv
70+ guardWith (show dctor ++ " is already defined") $
71+ not $ M.member (moduleName, dctor) (dataConstructors env)
72+
73+valueIsNotDefined :: ModuleName -> Ident -> Check ()
74+valueIsNotDefined moduleName name = do
75+ env <- getEnv
76+ case M.lookup (moduleName, name) (names env) of
77+ Just _ -> throwError $ show name ++ " is already defined"
78+ Nothing -> return ()
79+
80+addValue :: ModuleName -> Ident -> Type -> Check ()
81+addValue moduleName name ty = do
82+ env <- getEnv
83+ putEnv (env { names = M.insert (moduleName, name) (ty, Value) (names env) })
84+
38typeCheckAll :: ModuleName -> [Declaration] -> Check ()
85typeCheckAll :: ModuleName -> [Declaration] -> Check ()
39typeCheckAll _ [] = return ()
86typeCheckAll _ [] = return ()
40typeCheckAll moduleName (DataDeclaration name args dctors : rest) = do
87typeCheckAll moduleName (DataDeclaration name args dctors : rest) = do
41 rethrow (("Error in type constructor " ++ show name ++ ":\n") ++) $ do
88 rethrow (("Error in type constructor " ++ show name ++ ":\n") ++) $ do
42− env <- getEnv
89+ typeIsNotDefined moduleName name
43− guardWith (show name ++ " is already defined") $ not $ M.member (moduleName, name) (types env)
44− ctorKind <- kindsOf moduleName (Just name) args (mapMaybe snd dctors)
90+ ctorKind <- kindsOf moduleName name args (mapMaybe snd dctors)
45− putEnv $ env { types = M.insert (moduleName, name) (ctorKind, Data) (types env) }
91+ addDataType moduleName name args dctors ctorKind
46− forM_ dctors $ \(dctor, maybeTy) ->
92+ typeCheckAll moduleName rest
93+typeCheckAll moduleName (DataBindingGroupDeclaration tys : rest) = do
47− rethrow (("Error in data constructor " ++ show name ++ ":\n") ++) $ do
94+ rethrow (("Error in data binding group " ++ show (map (\(name, _, _) -> name) tys) ++ ":\n") ++) $ do
48− env' <- getEnv
95+ forM_ tys $ \(name, _, _) ->
49− guardWith (show dctor ++ " is already defined") $ not $ M.member (moduleName, dctor) (dataConstructors env')
96+ typeIsNotDefined moduleName name
50− let retTy = foldl TypeApp (TypeConstructor (Qualified (Just moduleName) name)) (map TypeVar args)
97+ ks <- kindsOfAll moduleName (map (\(name, args, dctors) -> (name, args, mapMaybe snd dctors)) tys)
51− let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy
98+ forM (zip tys ks) $ \((name, args, dctors), ctorKind) ->
52− let polyType = mkForAll args dctorTy
99+ addDataType moduleName name args dctors ctorKind
53− putEnv $ env' { dataConstructors = M.insert (moduleName, dctor) polyType (dataConstructors env') }
54 typeCheckAll moduleName rest
100 typeCheckAll moduleName rest
55−typeCheckAll moduleName (DataBindingGroupDeclaration tys : rest) = error (show tys)
56typeCheckAll moduleName (TypeSynonymDeclaration name args ty : rest) = do
101typeCheckAll moduleName (TypeSynonymDeclaration name args ty : rest) = do
57 rethrow (("Error in type synonym " ++ show name ++ ":\n") ++) $ do
102 rethrow (("Error in type synonym " ++ show name ++ ":\n") ++) $ do
58− env <- getEnv
103+ typeIsNotDefined moduleName name
59− guardWith (show name ++ " is already defined") $ not $ M.member (moduleName, name) (types env)
60− kind <- kindsOf moduleName (Just name) args [ty]
104+ kind <- kindsOf moduleName name args [ty]
61− putEnv $ env { types = M.insert (moduleName, name) (kind, TypeSynonym) (types env)
62− , typeSynonyms = M.insert (moduleName, name) (args, ty) (typeSynonyms env) }
105+ addTypeSynonym moduleName name args ty kind
63 typeCheckAll moduleName rest
106 typeCheckAll moduleName rest
64typeCheckAll _ (TypeDeclaration _ _ : _) = error "Type declarations should have been removed"
107typeCheckAll _ (TypeDeclaration _ _ : _) = error "Type declarations should have been removed"
65typeCheckAll moduleName (ValueDeclaration name [] Nothing val : rest) = do
108typeCheckAll moduleName (ValueDeclaration name [] Nothing val : rest) = do
66 rethrow (("Error in declaration " ++ show name ++ ":\n") ++) $ do
109 rethrow (("Error in declaration " ++ show name ++ ":\n") ++) $ do
67− env <- getEnv
68− case M.lookup (moduleName, name) (names env) of
110+ valueIsNotDefined moduleName name
69− Just _ -> throwError $ show name ++ " is already defined"
70− Nothing -> do
71− [ty] <- typesOf moduleName [(name, val)]
111+ [ty] <- typesOf moduleName [(name, val)]
72− putEnv (env { names = M.insert (moduleName, name) (ty, Value) (names env) })
112+ addValue moduleName name ty
73 typeCheckAll moduleName rest
113 typeCheckAll moduleName rest
74typeCheckAll _ (ValueDeclaration _ _ _ _ : _) = error "Binders were not desugared"
114typeCheckAll _ (ValueDeclaration _ _ _ _ : _) = error "Binders were not desugared"
75typeCheckAll moduleName (BindingGroupDeclaration vals : rest) = do
115typeCheckAll moduleName (BindingGroupDeclaration vals : rest) = do
76 rethrow (("Error in binding group " ++ show (map fst vals) ++ ":\n") ++) $ do
116 rethrow (("Error in binding group " ++ show (map fst vals) ++ ":\n") ++) $ do
77− forM_ (map fst vals) $ \name -> do
117+ forM_ (map fst vals) $ \name ->
78− env <- getEnv
118+ valueIsNotDefined moduleName name
79− case M.lookup (moduleName, name) (names env) of
80− Just _ -> throwError $ show name ++ " is already defined"
81− Nothing -> return ()
82 tys <- typesOf moduleName vals
119 tys <- typesOf moduleName vals
83 forM (zip (map fst vals) tys) $ \(name, ty) ->
120 forM (zip (map fst vals) tys) $ \(name, ty) ->
84− modifyEnv $ \env -> env { names = M.insert (moduleName, name) (ty, Value) (names env) }
121+ addValue moduleName name ty
85 typeCheckAll moduleName rest
122 typeCheckAll moduleName rest
86typeCheckAll moduleName (ExternDataDeclaration name kind : rest) = do
123typeCheckAll moduleName (ExternDataDeclaration name kind : rest) = do
87 env <- getEnv
124 env <- getEnv
@@ -124,22 +161,22 @@ typeCheckAll currentModule (ImportDeclaration moduleName idents : rest) = do
124 guardWith ("Module " ++ show moduleName ++ " does not exist") $ moduleExists env
161 guardWith ("Module " ++ show moduleName ++ " does not exist") $ moduleExists env
125 case idents of
162 case idents of
126 Nothing -> do
163 Nothing -> do
127− bindIdents (map snd $ filterModule (names env)) env
164+ shadowIdents (map snd $ filterModule (names env)) env
128− bindTypes (map snd $ filterModule (types env)) env
165+ shadowTypes (map snd $ filterModule (types env)) env
129 Just idents' -> do
166 Just idents' -> do
130− bindIdents (lefts idents') env
167+ shadowIdents (lefts idents') env
131− bindTypes (rights idents') env
168+ shadowTypes (rights idents') env
132 typeCheckAll currentModule rest
169 typeCheckAll currentModule rest
133 where errorMessage = (("Error in import declaration " ++ show moduleName ++ ":\n") ++)
170 where errorMessage = (("Error in import declaration " ++ show moduleName ++ ":\n") ++)
134 filterModule = filter ((== moduleName) . fst) . M.keys
171 filterModule = filter ((== moduleName) . fst) . M.keys
135 moduleExists env = not (null (filterModule (names env))) || not (null (filterModule (types env)))
172 moduleExists env = not (null (filterModule (names env))) || not (null (filterModule (types env)))
136− bindIdents idents' env =
173+ shadowIdents idents' env =
137 forM_ idents' $ \ident -> do
174 forM_ idents' $ \ident -> do
138 guardWith (show currentModule ++ "." ++ show ident ++ " is already defined") $ (currentModule, ident) `M.notMember` names env
175 guardWith (show currentModule ++ "." ++ show ident ++ " is already defined") $ (currentModule, ident) `M.notMember` names env
139 case (moduleName, ident) `M.lookup` names env of
176 case (moduleName, ident) `M.lookup` names env of
140 Just (pt, _) -> modifyEnv (\e -> e { names = M.insert (currentModule, ident) (pt, Alias moduleName ident) (names e) })
177 Just (pt, _) -> modifyEnv (\e -> e { names = M.insert (currentModule, ident) (pt, Alias moduleName ident) (names e) })
141 Nothing -> throwError (show moduleName ++ "." ++ show ident ++ " is undefined")
178 Nothing -> throwError (show moduleName ++ "." ++ show ident ++ " is undefined")
142− bindTypes pns env =
179+ shadowTypes pns env =
143 forM_ pns $ \pn -> do
180 forM_ pns $ \pn -> do
144 guardWith (show currentModule ++ "." ++ show pn ++ " is already defined") $ (currentModule, pn) `M.notMember` types env
181 guardWith (show currentModule ++ "." ++ show pn ++ " is already defined") $ (currentModule, pn) `M.notMember` types env
145 case (moduleName, pn) `M.lookup` types env of
182 case (moduleName, pn) `M.lookup` types env of
src/Language/PureScript/TypeChecker/Kinds.hs+50−37
@@ -15,8 +15,9 @@
15{-# LANGUAGE DeriveDataTypeable #-}
15{-# LANGUAGE DeriveDataTypeable #-}
16
16
17module Language.PureScript.TypeChecker.Kinds (
17module Language.PureScript.TypeChecker.Kinds (
18+ kindOf,
18 kindsOf,
19 kindsOf,
19− kindOf
20+ kindsOfAll
20) where
21) where
21
22
22import Language.PureScript.Types
23import Language.PureScript.Types
@@ -55,13 +56,30 @@ instance Unifiable Kind where
55 unknowns _ = []
56 unknowns _ = []
56
57
57kindOf :: ModuleName -> Type -> Check Kind
58kindOf :: ModuleName -> Type -> Check Kind
58−kindOf moduleName ty = fmap (\(k, _, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer Nothing M.empty ty
59+kindOf moduleName ty = fmap (\(k, _, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty
59
60
60−kindsOf :: ModuleName -> Maybe ProperName -> [String] -> [Type] -> Check Kind
61+kindsOf :: ModuleName -> ProperName -> [String] -> [PolyType] -> Check Kind
61kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst (SubstContext moduleName) $ do
62kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst (SubstContext moduleName) $ do
62 tyCon <- fresh
63 tyCon <- fresh
63 kargs <- replicateM (length args) fresh
64 kargs <- replicateM (length args) fresh
64− ks <- inferAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args kargs)) ts
65+ let dict = (name, tyCon) : zip (map ProperName args) kargs
66+ bindLocalTypeVariables moduleName dict $
67+ solveTypes ts kargs tyCon
68+
69+kindsOfAll :: ModuleName -> [(ProperName, [String], [PolyType])] -> Check [Kind]
70+kindsOfAll moduleName tys = fmap (map starIfUnknown . (\(ks, _, _) -> ks)) . runSubst (SubstContext moduleName) $ do
71+ tyCons <- replicateM (length tys) fresh
72+ let dict = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons
73+ bindLocalTypeVariables moduleName dict $
74+ zipWithM (\tyCon (_, args, ts) -> do
75+ kargs <- replicateM (length args) fresh
76+ let argDict = zip (map ProperName args) kargs
77+ bindLocalTypeVariables moduleName argDict $
78+ solveTypes ts kargs tyCon) tyCons tys
79+
80+solveTypes :: [Type] -> [Kind] -> Kind -> Subst Kind
81+solveTypes ts kargs tyCon = do
82+ ks <- mapM infer ts
65 tyCon ~~ foldr FunKind Star kargs
83 tyCon ~~ foldr FunKind Star kargs
66 forM_ ks $ \k -> k ~~ Star
84 forM_ ks $ \k -> k ~~ Star
67 return tyCon
85 return tyCon
@@ -71,56 +89,51 @@ starIfUnknown (KUnknown _) = Star
71starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
89starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
72starIfUnknown k = k
90starIfUnknown k = k
73
91
74−inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst [Kind]
75−inferAll name m = mapM (infer name m)
76−
77−infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Kind
92+infer :: Type -> Subst Kind
78−infer name m (Array t) = do
93+infer (Array t) = do
79− k <- infer name m t
94+ k <- infer t
80 k ~~ Star
95 k ~~ Star
81 return Star
96 return Star
82−infer name m (Object row) = do
97+infer (Object row) = do
83− k <- inferRow name m row
98+ k <- inferRow row
84 k ~~ Row
99 k ~~ Row
85 return Star
100 return Star
86−infer name m (Function args ret) = do
101+infer (Function args ret) = do
87− ks <- inferAll name m args
102+ ks <- mapM infer args
88− k <- infer name m ret
103+ k <- infer ret
89 k ~~ Star
104 k ~~ Star
90 forM ks (~~ Star)
105 forM ks (~~ Star)
91 return Star
106 return Star
92−infer _ m (TypeVar v) =
107+infer (TypeVar v) = do
93− case M.lookup v m of
108+ moduleName <- substCurrentModule <$> ask
94− Just k -> return k
109+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
95− Nothing -> throwError $ "Unbound type variable " ++ v
96−infer (Just (name, k)) _ (TypeConstructor (Qualified Nothing pn)) | name == pn = return k
97−infer _ _ (TypeConstructor v) = do
110+infer (TypeConstructor v) = do
98 env <- liftCheck getEnv
111 env <- liftCheck getEnv
99 moduleName <- substCurrentModule `fmap` ask
112 moduleName <- substCurrentModule `fmap` ask
100 case M.lookup (qualify moduleName v) (types env) of
113 case M.lookup (qualify moduleName v) (types env) of
101 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
114 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
102 Just (kind, _) -> return kind
115 Just (kind, _) -> return kind
103−infer name m (TypeApp t1 t2) = do
116+infer (TypeApp t1 t2) = do
104 k0 <- fresh
117 k0 <- fresh
105− k1 <- infer name m t1
118+ k1 <- infer t1
106− k2 <- infer name m t2
119+ k2 <- infer t2
107 k1 ~~ FunKind k2 k0
120 k1 ~~ FunKind k2 k0
108 return k0
121 return k0
109−infer name m (ForAll ident ty) = do
122+infer (ForAll ident ty) = do
110 k <- fresh
123 k <- fresh
111− infer name (M.insert ident k m) ty
124+ moduleName <- substCurrentModule <$> ask
125+ bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty
112−infer _ _ _ = return Star
126+infer _ = return Star
113
127
114−inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Kind
128+inferRow :: Row -> Subst Kind
115−inferRow _ m (RowVar v) = do
129+inferRow (RowVar v) = do
116− case M.lookup v m of
130+ moduleName <- substCurrentModule <$> ask
117− Just k -> return k
131+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
118− Nothing -> throwError $ "Unbound row variable " ++ v
119−inferRow _ _ REmpty = return Row
132+inferRow REmpty = return Row
120−inferRow name m (RCons _ ty row) = do
133+inferRow (RCons _ ty row) = do
121− k1 <- infer name m ty
134+ k1 <- infer ty
122− k2 <- inferRow name m row
135+ k2 <- inferRow row
123 k1 ~~ Star
136 k1 ~~ Star
124 k2 ~~ Row
137 k2 ~~ Row
125 return Row
138 return Row
126−inferRow _ _ _ = error "Invalid row in inferRow"
139+inferRow _ = error "Invalid row in inferRow"
src/Language/PureScript/TypeChecker/Monad.hs+32−4
@@ -32,9 +32,18 @@ import Control.Monad.Reader
32
32
33import qualified Data.Map as M
33import qualified Data.Map as M
34
34
35+data NameKind
36+ = Value
37+ | Extern
38+ | Alias ModuleName Ident
35−data NameKind = Value | Extern | Alias ModuleName Ident | LocalVariable deriving Show
39+ | LocalVariable deriving Show
36−
40+
41+data TypeDeclarationKind
42+ = Data
43+ | ExternData
44+ | TypeSynonym
37−data TypeDeclarationKind = Data | ExternData | TypeSynonym | DataAlias ModuleName ProperName deriving Show
45+ | DataAlias ModuleName ProperName
46+ | LocalTypeVariable deriving Show
38
47
39data Environment = Environment
48data Environment = Environment
40 { names :: M.Map (ModuleName, Ident) (Type, NameKind)
49 { names :: M.Map (ModuleName, Ident) (Type, NameKind)
@@ -49,16 +58,28 @@ emptyEnvironment = Environment M.empty M.empty M.empty M.empty M.empty
49
58
50bindNames :: (MonadState CheckState m) => M.Map (ModuleName, Ident) (Type, NameKind) -> m a -> m a
59bindNames :: (MonadState CheckState m) => M.Map (ModuleName, Ident) (Type, NameKind) -> m a -> m a
51bindNames newNames action = do
60bindNames newNames action = do
52− orig <- get
61+ orig <- get
53 modify $ \st -> st { checkEnv = (checkEnv st) { names = newNames `M.union` (names . checkEnv $ st) } }
62 modify $ \st -> st { checkEnv = (checkEnv st) { names = newNames `M.union` (names . checkEnv $ st) } }
54 a <- action
63 a <- action
55 modify $ \st -> st { checkEnv = (checkEnv st) { names = names . checkEnv $ orig } }
64 modify $ \st -> st { checkEnv = (checkEnv st) { names = names . checkEnv $ orig } }
56 return a
65 return a
57
66
67+bindTypes :: (MonadState CheckState m) => M.Map (ModuleName, ProperName) (Kind, TypeDeclarationKind) -> m a -> m a
68+bindTypes newNames action = do
69+ orig <- get
70+ modify $ \st -> st { checkEnv = (checkEnv st) { types = newNames `M.union` (types . checkEnv $ st) } }
71+ a <- action
72+ modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }
73+ return a
74+
58bindLocalVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(Ident, Type)] -> m a -> m a
75bindLocalVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(Ident, Type)] -> m a -> m a
59bindLocalVariables moduleName bindings action =
76bindLocalVariables moduleName bindings action =
60 bindNames (M.fromList $ flip map bindings $ \(name, ty) -> ((moduleName, name), (ty, LocalVariable))) action
77 bindNames (M.fromList $ flip map bindings $ \(name, ty) -> ((moduleName, name), (ty, LocalVariable))) action
61
78
79+bindLocalTypeVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(ProperName, Kind)] -> m a -> m a
80+bindLocalTypeVariables moduleName bindings action =
81+ bindTypes (M.fromList $ flip map bindings $ \(name, k) -> ((moduleName, name), (k, LocalTypeVariable))) action
82+
62lookupVariable :: (Functor m, MonadState CheckState m, MonadError String m) => ModuleName -> Qualified Ident -> m Type
83lookupVariable :: (Functor m, MonadState CheckState m, MonadError String m) => ModuleName -> Qualified Ident -> m Type
63lookupVariable currentModule (Qualified moduleName var) = do
84lookupVariable currentModule (Qualified moduleName var) = do
64 env <- getEnv
85 env <- getEnv
@@ -66,6 +87,13 @@ lookupVariable currentModule (Qualified moduleName var) = do
66 Nothing -> throwError $ show var ++ " is undefined"
87 Nothing -> throwError $ show var ++ " is undefined"
67 Just (ty, _) -> return ty
88 Just (ty, _) -> return ty
68
89
90+lookupTypeVariable :: (Functor m, MonadState CheckState m, MonadError String m) => ModuleName -> Qualified ProperName -> m Kind
91+lookupTypeVariable currentModule (Qualified moduleName name) = do
92+ env <- getEnv
93+ case M.lookup (fromMaybe currentModule moduleName, name) (types env) of
94+ Nothing -> throwError $ "Type variable " ++ show name ++ " is undefined"
95+ Just (k, _) -> return k
96+
69data AnyUnifiable where
97data AnyUnifiable where
70 AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable
98 AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable
71
99