@@ -246,21 +246,22 @@ overTypes f = everywhere (mkT f)
246246replaceTypeClassDictionaries :: ModuleName -> Value -> Check Value
247247replaceTypeClassDictionaries mn = everywhereM' (mkM go)
248248 where
249− go (TypeClassDictionary constraint dicts) = entails mn dicts constraint
249+ go (TypeClassDictionary constraint dicts) = do
250+ env <- getEnv
251+ entails env mn dicts constraint
250252 go other = return other
251253
252254-- |
253255-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
254256-- return a type class dictionary reference.
255257--
256−entails :: ModuleName -> [TypeClassDictionaryInScope] -> (Qualified ProperName, [Type]) -> Check Value
257−entails moduleName context goal@(className, tys) = do
258− env <- getEnv
259− case go env goal of
258+entails :: Environment -> ModuleName -> [TypeClassDictionaryInScope] -> (Qualified ProperName, [Type]) -> Check Value
259+entails env moduleName context goal@(className, tys) = do
260+ case go goal of
260261 [] -> throwError $ "No " ++ show className ++ " instance found for " ++ intercalate ", " (map prettyPrintType tys)
261262 (dict : _) -> return dict
262263 where
263− go env (className', tys') =
264+ go (className', tys') =
264265 [ mkDictionary (canonicalizeDictionary tcd) args
265266 | tcd <- context
266267 -- Choose type class dictionaries in scope in the current module
@@ -270,14 +271,14 @@ entails moduleName context goal@(className, tys) = do
270271 -- Make sure the type unifies with the type in the type instance definition
271272 , subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
272273 -- Solve any necessary subgoals
273− , args <- solveSubgoals env subst (tcdDependencies tcd) ]
274+ , args <- solveSubgoals subst (tcdDependencies tcd) ]
274275 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
275276 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
276277 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
277− solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, [Type])] -> [Maybe [Value]]
278− solveSubgoals _ _ Nothing = return Nothing
279− solveSubgoals env subst (Just subgoals) = do
280− dict <- mapM (go env . second (map (replaceAllTypeVars subst))) subgoals
278+ solveSubgoals :: [(String, Type)] -> Maybe [(Qualified ProperName, [Type])] -> [Maybe [Value]]
279+ solveSubgoals _ Nothing = return Nothing
280+ solveSubgoals subst (Just subgoals) = do
281+ dict <- mapM (go . second (map (replaceAllTypeVars subst))) subgoals
281282 return $ Just dict
282283 -- Make a dictionary from subgoal dictionaries by applying the correct function
283284 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
@@ -293,20 +294,43 @@ entails moduleName context goal@(className, tys) = do
293294 verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]
294295 verifySubstitution subst = do
295296 let grps = groupBy ((==) `on` fst) subst
296− guard (all ((==) 1 . length . nubBy ((==) `on` snd)) grps)
297+ guard (all (pairwise (unifiesWith env) . map snd) grps)
297298 return $ map head grps
298299
300+-- |
301+-- Check all values in a list pairwise match a predicate
302+--
303+pairwise :: (a -> a -> Bool) -> [a] -> Bool
304+pairwise _ [] = True
305+pairwise _ [_] = True
306+pairwise p (x : xs) = all (p x) xs && pairwise p xs
307+
308+-- |
309+-- Check that two types unify
310+--
311+unifiesWith :: Environment -> Type -> Type -> Bool
312+unifiesWith _ (TUnknown _) _ = True
313+unifiesWith _ _ (TUnknown _) = True
314+unifiesWith _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = True
315+unifiesWith _ (TypeVar v1) (TypeVar v2) | v1 == v2 = True
316+unifiesWith _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = True
317+unifiesWith e (TypeApp h1 t1) (TypeApp h2 t2) = unifiesWith e h1 h2 && unifiesWith e t1 t2
318+unifiesWith e (SaturatedTypeSynonym name args) t2 =
319+ case expandTypeSynonym' e name args of
320+ Left _ -> False
321+ Right t1 -> unifiesWith e t1 t2
322+unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1
323+unifiesWith _ _ _ = False
324+
299325-- |
300326-- Check whether the type heads of two types are equal (for the purposes of type class dictionary lookup),
301327-- and return a substitution from type variables to types which makes the type heads unify.
302328--
303329typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
304330typeHeadsAreEqual _ _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = Just []
305−typeHeadsAreEqual _ _ (TypeVar v) t = Just [(v, t)]
306331typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
307332typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
308−typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2
309−typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1
333+typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
310334typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
311335 Left _ -> Nothing
312336 Right t1 -> typeHeadsAreEqual m e t1 t2