@@ -267,22 +267,33 @@ entails moduleName context goal@(className, ty) = do
267267 go env (className', ty') =
268268 [ mkDictionary (canonicalizeDictionary tcd) args
269269 | tcd <- context
270+ -- Choose type class dictionaries in scope in the current module
270271 , filterModule tcd
272+ -- Make sure the type class name matches the one we are trying to satisfy
271273 , typeConstructorsAreEqual env moduleName className' (tcdClassName tcd)
274+ -- Make sure the type unifies with the type in the type instance definition
272275 , subst <- maybeToList $ typeHeadsAreEqual moduleName env ty' (tcdInstanceType tcd)
276+ -- Solve any necessary subgoals
273277 , 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.
274281 solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
275282 solveSubgoals _ _ Nothing = return Nothing
276283 solveSubgoals env subst (Just subgoals) = do
277284 dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
278285 return $ Just dict
286+ -- Make a dictionary from subgoal dictionaries by applying the correct function
279287 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
280288 mkDictionary fnName Nothing = Var fnName
281289 mkDictionary fnName (Just dicts) = foldl App (Var fnName) dicts
290+ -- Filter out type dictionaries which are in scope in the current module
282291 filterModule :: TypeClassDictionaryInScope -> Bool
283292 filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True
284293 filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
285294 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
286297 canonicalizeDictionary :: TypeClassDictionaryInScope -> Qualified Ident
287298 canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDRegular, tcdName = nm }) = nm
288299 canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDAlias nm }) = nm
@@ -327,6 +338,12 @@ findAllTypes = everything (++) (mkQ [] go)
327338skolemEscapeCheck :: Value -> Check ()
328339skolemEscapeCheck (TypedValue False _ _) = return ()
329340skolemEscapeCheck 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.
330347 case everythingWithContext [] (++) (mkQ ((,) []) go) root of
331348 [] -> return ()
332349 ((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
382399replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
383400
384401-- |
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.
404+--
405+-- This is necessary during type checking to avoid unifying a polymorphic type with a
406+-- unification variable.
386407--
387408instantiatePolyTypeWithUnknowns :: Value -> Type -> UnifyT Type Check (Value, Type)
388409instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do