@@ -246,21 +246,22 @@ overTypes f = everywhere (mkT f)
246replaceTypeClassDictionaries :: ModuleName -> Value -> Check Value
246replaceTypeClassDictionaries :: ModuleName -> Value -> Check Value
247replaceTypeClassDictionaries mn = everywhereM' (mkM go)
247replaceTypeClassDictionaries mn = everywhereM' (mkM go)
249− go (TypeClassDictionary constraint dicts) = entails mn dicts constraint
249+ go (TypeClassDictionary constraint dicts) = do
251+ entails env mn dicts constraint
250 go other = return other
252 go other = return other
253-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
255-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
254-- return a type class dictionary reference.
256-- return a type class dictionary reference.
256−entails :: ModuleName -> [TypeClassDictionaryInScope] -> (Qualified ProperName, [Type]) -> Check Value
258+entails :: Environment -> ModuleName -> [TypeClassDictionaryInScope] -> (Qualified ProperName, [Type]) -> Check Value
257−entails moduleName context goal@(className, tys) = do
259+entails env moduleName context goal@(className, tys) = do
259− case go env goal of
260+ case go goal of
260 [] -> throwError $ "No " ++ show className ++ " instance found for " ++ intercalate ", " (map prettyPrintType tys)
261 [] -> throwError $ "No " ++ show className ++ " instance found for " ++ intercalate ", " (map prettyPrintType tys)
261 (dict : _) -> return dict
262 (dict : _) -> return dict
263− go env (className', tys') =
264+ go (className', tys') =
264 [ mkDictionary (canonicalizeDictionary tcd) args
265 [ mkDictionary (canonicalizeDictionary tcd) args
265 | tcd <- context
266 | tcd <- context
266 -- Choose type class dictionaries in scope in the current module
267 -- Choose type class dictionaries in scope in the current module
@@ -270,14 +271,14 @@ entails moduleName context goal@(className, tys) = do
270 -- Make sure the type unifies with the type in the type instance definition
271 -- Make sure the type unifies with the type in the type instance definition
271 , subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
272 , subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
272 -- Solve any necessary subgoals
273 -- Solve any necessary subgoals
273− , args <- solveSubgoals env subst (tcdDependencies tcd) ]
274+ , args <- solveSubgoals subst (tcdDependencies tcd) ]
274 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
275 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
275 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
276 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
276 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
277 -- 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 :: [(String, Type)] -> Maybe [(Qualified ProperName, [Type])] -> [Maybe [Value]]
278− solveSubgoals _ _ Nothing = return Nothing
279+ solveSubgoals _ Nothing = return Nothing
279− solveSubgoals env subst (Just subgoals) = do
280+ solveSubgoals subst (Just subgoals) = do
280− dict <- mapM (go env . second (map (replaceAllTypeVars subst))) subgoals
281+ dict <- mapM (go . second (map (replaceAllTypeVars subst))) subgoals
281 return $ Just dict
282 return $ Just dict
282 -- Make a dictionary from subgoal dictionaries by applying the correct function
283 -- Make a dictionary from subgoal dictionaries by applying the correct function
283 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
284 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
@@ -293,20 +294,43 @@ entails moduleName context goal@(className, tys) = do
293 verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]
294 verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]
294 verifySubstitution subst = do
295 verifySubstitution subst = do
295 let grps = groupBy ((==) `on` fst) subst
296 let grps = groupBy ((==) `on` fst) subst
296− guard (all ((==) 1 . length . nubBy ((==) `on` snd)) grps)
297+ guard (all (pairwise (unifiesWith env) . map snd) grps)
297 return $ map head grps
298 return $ map head grps
301+-- Check all values in a list pairwise match a predicate
303+pairwise :: (a -> a -> Bool) -> [a] -> Bool
305+pairwise _ [_] = True
306+pairwise p (x : xs) = all (p x) xs && pairwise p xs
309+-- Check that two types unify
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
321+ Right t1 -> unifiesWith e t1 t2
322+unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1
323+unifiesWith _ _ _ = False
300-- Check whether the type heads of two types are equal (for the purposes of type class dictionary lookup),
326-- Check whether the type heads of two types are equal (for the purposes of type class dictionary lookup),
301-- and return a substitution from type variables to types which makes the type heads unify.
327-- and return a substitution from type variables to types which makes the type heads unify.
303typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
329typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
304typeHeadsAreEqual _ _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = Just []
330typeHeadsAreEqual _ _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = Just []
305−typeHeadsAreEqual _ _ (TypeVar v) t = Just [(v, t)]
306typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
331typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
307typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
332typeHeadsAreEqual _ _ (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
333+typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
309−typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1
310typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
334typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
311 Left _ -> Nothing
335 Left _ -> Nothing
312 Right t1 -> typeHeadsAreEqual m e t1 t2
336 Right t1 -> typeHeadsAreEqual m e t1 t2