@@ -76,11 +76,11 @@ entails env moduleName context = solve
76 (subst, tcd) <- unique instances
76 (subst, tcd) <- unique instances
77 -- Solve any necessary subgoals
77 -- Solve any necessary subgoals
78 args <- solveSubgoals subst (tcdDependencies tcd)
78 args <- solveSubgoals subst (tcdDependencies tcd)
79− return $ foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)
79+ return $ foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)
80− (mkDictionary (canonicalizeDictionary tcd) args)
80+ (mkDictionary (canonicalizeDictionary tcd) args)
81 (tcdPath tcd)
81 (tcdPath tcd)
84 unique :: [(a, TypeClassDictionaryInScope)] -> Check (a, TypeClassDictionaryInScope)
84 unique :: [(a, TypeClassDictionaryInScope)] -> Check (a, TypeClassDictionaryInScope)
85 unique [] = throwError . errorMessage $ NoInstanceFound className' tys'
85 unique [] = throwError . errorMessage $ NoInstanceFound className' tys'
86 unique [a] = return a
86 unique [a] = return a
@@ -109,13 +109,13 @@ entails env moduleName context = solve
109 solveSubgoals subst (Just subgoals) = do
109 solveSubgoals subst (Just subgoals) = do
110 dict <- mapM (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
110 dict <- mapM (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
111 return $ Just dict
111 return $ Just dict
113 -- Make a dictionary from subgoal dictionaries by applying the correct function
113 -- Make a dictionary from subgoal dictionaries by applying the correct function
114 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
114 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
115 mkDictionary fnName Nothing = LocalDictionaryValue fnName
115 mkDictionary fnName Nothing = LocalDictionaryValue fnName
116 mkDictionary fnName (Just []) = GlobalDictionaryValue fnName
116 mkDictionary fnName (Just []) = GlobalDictionaryValue fnName
117 mkDictionary fnName (Just dicts) = DependentDictionaryValue fnName dicts
117 mkDictionary fnName (Just dicts) = DependentDictionaryValue fnName dicts
119 -- Turn a DictionaryValue into a Expr
119 -- Turn a DictionaryValue into a Expr
120 dictionaryValueToValue :: DictionaryValue -> Expr
120 dictionaryValueToValue :: DictionaryValue -> Expr
121 dictionaryValueToValue (LocalDictionaryValue fnName) = Var fnName
121 dictionaryValueToValue (LocalDictionaryValue fnName) = Var fnName
@@ -128,10 +128,10 @@ entails env moduleName context = solve
128 -- Ensure that a substitution is valid
128 -- Ensure that a substitution is valid
129 verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]
129 verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]
130 verifySubstitution subst = do
130 verifySubstitution subst = do
131− let grps = groupBy ((==) `on` fst) subst
131+ let grps = groupBy ((==) `on` fst) . sortBy (compare `on` fst) $ subst
132 guard (all (pairwise (unifiesWith env) . map snd) grps)
132 guard (all (pairwise (unifiesWith env) . map snd) grps)
133 return $ map head grps
133 return $ map head grps
135 valUndefined :: Expr
135 valUndefined :: Expr
136 valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))
136 valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))
@@ -143,7 +143,7 @@ typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String
143typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
143typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
144typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
144typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
145typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
145typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
146−typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2
146+typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2
147 <*> typeHeadsAreEqual m e t1 t2
147 <*> typeHeadsAreEqual m e t1 t2
148typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
148typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
149 Left _ -> Nothing
149 Left _ -> Nothing
@@ -152,16 +152,16 @@ typeHeadsAreEqual _ _ REmpty REmpty = Just []
152typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
152typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
153 let (s1, r1') = rowToList r1
153 let (s1, r1') = rowToList r1
154 (s2, r2') = rowToList r2
154 (s2, r2') = rowToList r2
156 int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
156 int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
157 sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
157 sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
158 sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
158 sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
159− in (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int
159+ in (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int
160 <*> go sd1 r1' sd2 r2'
160 <*> go sd1 r1' sd2 r2'
162 go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
162 go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
163− go [] REmpty [] REmpty = Just []
163+ go [] REmpty [] REmpty = Just []
164− go [] (TUnknown _) _ _ = Just []
164+ go [] (TUnknown _) _ _ = Just []
165 go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
165 go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
166 go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
166 go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
167 go sd r [] (TypeVar v) = Just [(v, rowFromList (sd, r))]
167 go sd r [] (TypeVar v) = Just [(v, rowFromList (sd, r))]