@@ -267,22 +267,33 @@ entails moduleName context goal@(className, ty) = do
267 go env (className', ty') =
267 go env (className', ty') =
268 [ mkDictionary (canonicalizeDictionary tcd) args
268 [ mkDictionary (canonicalizeDictionary tcd) args
269 | tcd <- context
269 | tcd <- context
270+ -- Choose type class dictionaries in scope in the current module
270 , filterModule tcd
271 , filterModule tcd
272+ -- Make sure the type class name matches the one we are trying to satisfy
271 , typeConstructorsAreEqual env moduleName className' (tcdClassName tcd)
273 , typeConstructorsAreEqual env moduleName className' (tcdClassName tcd)
274+ -- Make sure the type unifies with the type in the type instance definition
272 , subst <- maybeToList $ typeHeadsAreEqual moduleName env ty' (tcdInstanceType tcd)
275 , subst <- maybeToList $ typeHeadsAreEqual moduleName env ty' (tcdInstanceType tcd)
276+ -- Solve any necessary subgoals
273 , args <- solveSubgoals env subst (tcdDependencies tcd) ]
277 , args <- solveSubgoals env subst (tcdDependencies tcd) ]
278+ -- Create dictionaries for subgoals which still need to be solved by calling go recursively
279+ -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
280+ -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
274 solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
281 solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
275 solveSubgoals _ _ Nothing = return Nothing
282 solveSubgoals _ _ Nothing = return Nothing
276 solveSubgoals env subst (Just subgoals) = do
283 solveSubgoals env subst (Just subgoals) = do
277 dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
284 dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
278 return $ Just dict
285 return $ Just dict
286+ -- Make a dictionary from subgoal dictionaries by applying the correct function
279 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
287 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
280 mkDictionary fnName Nothing = Var fnName
288 mkDictionary fnName Nothing = Var fnName
281 mkDictionary fnName (Just dicts) = foldl App (Var fnName) dicts
289 mkDictionary fnName (Just dicts) = foldl App (Var fnName) dicts
290+ -- Filter out type dictionaries which are in scope in the current module
282 filterModule :: TypeClassDictionaryInScope -> Bool
291 filterModule :: TypeClassDictionaryInScope -> Bool
283 filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True
292 filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True
284 filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
293 filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
285 filterModule _ = False
294 filterModule _ = False
295+ -- Resolve a type class dictionary in scope to an actual value by following any (TCDAlias) pointers
296+ -- which originated from module imports
286 canonicalizeDictionary :: TypeClassDictionaryInScope -> Qualified Ident
297 canonicalizeDictionary :: TypeClassDictionaryInScope -> Qualified Ident
287 canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDRegular, tcdName = nm }) = nm
298 canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDRegular, tcdName = nm }) = nm
288 canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDAlias nm }) = nm
299 canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDAlias nm }) = nm
@@ -327,6 +338,12 @@ findAllTypes = everything (++) (mkQ [] go)
327skolemEscapeCheck :: Value -> Check ()
338skolemEscapeCheck :: Value -> Check ()
328skolemEscapeCheck (TypedValue False _ _) = return ()
339skolemEscapeCheck (TypedValue False _ _) = return ()
329skolemEscapeCheck root@(TypedValue _ _ _) =
340skolemEscapeCheck root@(TypedValue _ _ _) =
341+ -- Every skolem variable is created when a ForAll type is skolemized.
342+ -- This determines the scope of that skolem variable, which is copied from the SkolemScope
343+ -- field of the ForAll constructor.
344+ -- We traverse the tree top-down, and collect any SkolemScopes introduced by ForAlls.
345+ -- If a Skolem is encountered whose SkolemScope is not in the current list, we have found
346+ -- an escaped skolem variable.
330 case everythingWithContext [] (++) (mkQ ((,) []) go) root of
347 case everythingWithContext [] (++) (mkQ ((,) []) go) root of
331 [] -> return ()
348 [] -> return ()
332 ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ maybe "<unknown>" prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val
349 ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ maybe "<unknown>" prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val
@@ -382,7 +399,11 @@ replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
382replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
399replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
385−-- Replace named type variables with new unification variables
402+-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
403+-- or TypeClassDictionary values.
405+-- This is necessary during type checking to avoid unifying a polymorphic type with a
406+-- unification variable.
387instantiatePolyTypeWithUnknowns :: Value -> Type -> UnifyT Type Check (Value, Type)
408instantiatePolyTypeWithUnknowns :: Value -> Type -> UnifyT Type Check (Value, Type)
388instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
409instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do