@@ -20,6 +20,7 @@ module Language.PureScript.TypeChecker.Entailment (
20import Data.Function (on)
20import Data.Function (on)
21import Data.List
21import Data.List
22import Data.Maybe (maybeToList)
22import Data.Maybe (maybeToList)
23+import Data.Foldable (foldMap)
23import qualified Data.Map as M
24import qualified Data.Map as M
25import Control.Applicative
26import Control.Applicative
@@ -199,13 +200,32 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt
199-- and return a substitution from type variables to types which makes the type heads unify.
200-- and return a substitution from type variables to types which makes the type heads unify.
201typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
202typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
202−typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
203+typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
203−typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
204+typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
204typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
205typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
205−typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
206+typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2
207+ <*> typeHeadsAreEqual m e t1 t2
206typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
208typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
207 Left _ -> Nothing
209 Left _ -> Nothing
208 Right t1 -> typeHeadsAreEqual m e t1 t2
210 Right t1 -> typeHeadsAreEqual m e t1 t2
211+typeHeadsAreEqual _ _ REmpty REmpty = Just []
212+typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
213+ let (s1, r1') = rowToList r1
214+ (s2, r2') = rowToList r2
216+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
217+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
218+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
219+ in (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int
220+ <*> go sd1 r1' sd2 r2'
222+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
223+ go [] REmpty [] REmpty = Just []
224+ go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
225+ go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
226+ go _ (TUnknown _) _ _ = Just []
227+ go _ _ _ (TUnknown _) = Just []
228+ go _ _ _ _ = Nothing
209typeHeadsAreEqual _ _ _ _ = Nothing
229typeHeadsAreEqual _ _ _ _ = Nothing