@@ -202,6 +202,9 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt
202202typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
203203typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
204204typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
205+-- In this case, we want might want type information to flow back to the typechecker.
206+-- TODO: run this function in the UnifyT monad.
207+typeHeadsAreEqual _ _ (TUnknown _) _ = Just []
205208typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
206209typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2
207210 <*> typeHeadsAreEqual m e t1 t2
@@ -221,10 +224,14 @@ typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
221224 where
222225 go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
223226 go [] REmpty [] REmpty = Just []
227+ go [] (TUnknown _) _ _ = Just []
224228 go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
225229 go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
226− go _ (TUnknown _) _ _ = Just []
227− go _ _ _ (TUnknown _) = Just []
230+ go sd r [] (TypeVar v) = Just [(v, rowFromList (sd, r))]
231+ -- Technically, this case should result in solved variables. Until the constraint
232+ -- solver runs in the UnifyT monad, this just means that some (unusual) instances
233+ -- will not be found.
234+ go _ (TypeVar _) _ (TypeVar _) = Just []
228235 go _ _ _ _ = Nothing
229236typeHeadsAreEqual _ _ _ _ = Nothing
230237