@@ -167,40 +167,70 @@ typeConstructorsAreEqual env moduleName = (==) `on` canonicalizeType moduleName
167typesOf :: ModuleName -> [(Ident, Value)] -> Check [(Ident, (Value, Type))]
167typesOf :: ModuleName -> [(Ident, Value)] -> Check [(Ident, (Value, Type))]
168typesOf moduleName vals = do
168typesOf moduleName vals = do
169 tys <- fmap tidyUp . liftUnify $ do
169 tys <- fmap tidyUp . liftUnify $ do
171+ -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed
170− let es = map isTyped vals
172+ es = map isTyped vals
173+ -- Filter the typed and untyped declarations
171− typed = filter (isJust . snd . snd) es
174+ typed = filter (isJust . snd . snd) es
172− untyped = filter (isNothing . snd . snd) es
175+ untyped = filter (isNothing . snd . snd) es
176+ -- Make a map of names to typed declarations
173− typedDict = map (\(ident, (_, Just ty)) -> (ident, ty)) typed
177+ typedDict = map (\(ident, (_, Just (ty, _))) -> (ident, ty)) typed
178+ -- Create fresh unification variables for the types of untyped declarations
174 untypedNames <- replicateM (length untyped) fresh
179 untypedNames <- replicateM (length untyped) fresh
181+ -- Make a map of names to the unification variables of untyped declarations
175− let untypedDict = zip (map fst untyped) untypedNames
182+ untypedDict = zip (map fst untyped) untypedNames
183+ -- Create the dictionary of all name/type pairs, which will be added to the environment during type checking
176− dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ (map (id *** fst) typedDict) ++ untypedDict)
184+ dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ typedDict ++ untypedDict)
177− forM es $ \e -> do
185+ forM es $ \e@(_, (val, _)) -> do
186+ -- If the declaration is a function, it has access to other values in the binding group.
187+ -- If not, the generated code might fail at runtime since those values might be undefined.
188+ let dict' = if isFunction val then dict else M.empty
178 triple@(_, (val, ty)) <- case e of
189 triple@(_, (val, ty)) <- case e of
190+ -- Typed declarations
179 (ident, (val, Just (ty, checkType))) -> do
191 (ident, (val, Just (ty, checkType))) -> do
180 kind <- liftCheck $ kindOf moduleName ty
193 kind <- liftCheck $ kindOf moduleName ty
181 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
194 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
195+ -- Check the type with the new names in scope
182 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
196 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
183− val' <- bindNames dict $ if checkType
197+ val' <- bindNames dict' $ if checkType
184 then TypedValue True <$> check val ty' <*> pure ty'
198 then TypedValue True <$> check val ty' <*> pure ty'
185 else return (TypedValue False val ty')
199 else return (TypedValue False val ty')
186 return (ident, (val', ty'))
200 return (ident, (val', ty'))
201+ -- Untyped declarations
187 (ident, (val, Nothing)) -> do
202 (ident, (val, Nothing)) -> do
203+ -- Infer the type with the new names in scope
188− TypedValue _ val' ty <- bindNames dict $ infer val
204+ TypedValue _ val' ty <- bindNames dict' $ infer val
189 ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
205 ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
190 return (ident, (TypedValue True val' ty, ty))
206 return (ident, (TypedValue True val' ty, ty))
207+ -- If run-main is enabled, need to check that Main.main has type Eff eff a for some eff, a
191 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do
208 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do
192 [eff, a] <- replicateM 2 fresh
209 [eff, a] <- replicateM 2 fresh
193 ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
210 ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
211+ -- Make sure unification variables do not escape
194 escapeCheck val ty
212 escapeCheck val ty
195 return triple
213 return triple
196− forM tys $ \(ident, (val, ty)) -> do
214+ forM tys $ \(ident, (val, ty)) -> rethrow (("Error in " ++ show ident ++ ": \n") ++) $ do
215+ -- Replace type class dictionary placeholders with actual dictionaries
197 val' <- replaceTypeClassDictionaries moduleName val
216 val' <- replaceTypeClassDictionaries moduleName val
217+ -- Check skolem variables did not escape their scope
198− rethrow (("Error in " ++ show ident ++ ": \n") ++) $ skolemEscapeCheck val'
218+ skolemEscapeCheck val'
199 return $ (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'
220 return $ (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'
200 , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))
221 , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))
223+ -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
202 tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
224 tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
227+-- Check if a value introduces a function
229+isFunction :: Value -> Bool
230+isFunction (Abs _ _) = True
231+isFunction (TypedValue _ val _) = isFunction val
205-- Check if a value contains a type annotation
235-- Check if a value contains a type annotation