@@ -48,7 +48,7 @@ constrain env (L _ _ expr) tipe =
4848 exists $ \t2 -> do
4949 fragment <- Pattern.constrain env p t1
5050 c2 <- constrain env e t2
51− let c = ex (vars fragment) (CLet [Scheme [] [] CTrue (typeEnv fragment)]
51+ let c = ex (vars fragment) (CLet [monoscheme (typeEnv fragment)]
5252 (typeConstraint fragment /\ c2 ))
5353 return $ c /\ tipe === (t1 ==> t2)
5454
@@ -66,8 +66,6 @@ constrain env (L _ _ expr) tipe =
6666 ce <- constrain env e tipe
6767 return (cb /\ ce)
6868
69− Let defs body -> error "not defined yet"
70−
7169 Case e branches ->
7270 exists $ \t -> do
7371 ce <- constrain env e t
@@ -75,7 +73,7 @@ constrain env (L _ _ expr) tipe =
7573 fragment <- Pattern.constrain env p t
7674 c <- constrain env e tipe
7775 return $ ex (vars fragment)
78− (CLet [Scheme [] [] CTrue (typeEnv fragment)]
76+ (CLet [monoscheme (typeEnv fragment)]
7977 (typeConstraint fragment /\ c))
8078 CAnd . (:) ce <$> mapM branch branches
8179
@@ -140,16 +138,62 @@ constrain env (L _ _ expr) tipe =
140138 Markdown _ ->
141139 return $ tipe === Env.get env builtin "Element"
142140
141+ Let defs body ->
142+ do c <- constrain env body tipe
143+ (schemes, rqs, fqs, header, c2, c1) <-
144+ Monad.foldM (constrainDef env)
145+ ([], [], [], Map.empty, CTrue, CTrue)
146+ (collapseDefs defs)
147+ return $ CLet schemes
148+ (CLet [Scheme rqs fqs (CLet [monoscheme header] c2) header ]
149+ (c1 /\ c))
150+
151+
152+constrainDef env info (name, args, expr, maybeTipe) =
153+ let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
154+ case maybeTipe of
155+ Just tipe ->
156+ do flexiVars <- mapM (\_ -> flexibleVar) args
157+ let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) args flexiVars
158+ env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
159+ typ = error "This should be the internal representation of the user defined type."
160+ scheme = Scheme { rigidQuantifiers = [],
161+ flexibleQuantifiers = flexiVars,
162+ constraint = CTrue,
163+ header = Map.singleton name typ }
164+ c <- constrain env' expr typ
165+ return ( scheme : schemes
166+ , rigidQuantifiers
167+ , flexibleQuantifiers
168+ , headers
169+ , c2
170+ , fl rigidQuantifiers c /\ c1 )
171+
172+ Nothing ->
173+ do var <- flexibleVar
174+ rigidVars <- mapM (\_ -> rigidVar) args
175+ let tipe = VarN var
176+ inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) args rigidVars
177+ env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
178+ c <- constrain env' expr tipe
179+ return ( schemes
180+ , rigidVars ++ rigidQuantifiers
181+ , var : flexibleQuantifiers
182+ , Map.insert name tipe headers
183+ , c /\ c2
184+ , c1 )
143185
144186--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
145−collapseDefs = go Map.empty Map.empty
146− where
147− go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
148− (Map.map ($ Nothing) (Map.difference defs typs))
149− go defs typs (d:ds) =
150− case d of
151− Def name args body ->
152− go (Map.insert name ((,,) args body) defs) typs ds
153− TypeAnnotation name typ ->
154− go defs (Map.insert name typ typs) ds
155−
187+collapseDefs definitions =
188+ map (\(name, (args, expr, tipe)) -> (name, args, expr, tipe)) defPairs
189+ where
190+ defPairs = Map.toList (go Map.empty Map.empty definitions)
191+
192+ go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
193+ (Map.map ($ Nothing) (Map.difference defs typs))
194+ go defs typs (d:ds) =
195+ case d of
196+ Def name args body ->
197+ go (Map.insert name ((,,) args body) defs) typs ds
198+ TypeAnnotation name typ ->
199+ go defs (Map.insert name typ typs) ds