Skip to content

Fix entailment issues with skolems and matches #3121

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
LiamGoodacre merged 1 commit into from
Oct 21, 2017
Merged

Fix entailment issues with skolems and matches #3121

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions examples/failing/InstanceChainBothUnknownAndMatch.purs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
-- @shouldFailWith NoInstanceFound
module InstanceChains.BothUnknownAndMatch where

class Same l r o | l r -> o
instance sameY :: Same t t @"Y" else instance sameN :: Same l r @"N"

@paf31 paf31 Oct 20, 2017

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, well there's the kind error again :(

@paf31 paf31 Oct 20, 2017

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh wait, no, I didn't see the proxy :)

same :: forall l r o. Same l r o => l -> r -> @o
same _ _ = @o

-- for label `u`, `t ~ Int` should be Unknown
-- for label `m`, `Int ~ Int` should be a match
-- together they should be Unknown
example :: forall t. @t -> @_
example _ = same @(u :: t, m :: Int) @(u :: Int, m :: Int)

@paf31 paf31 Oct 20, 2017

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But this is a kind error, surely?

@LiamGoodacre LiamGoodacre Oct 20, 2017

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note to readers: when this comment was made, same had type forall l r o. Same l r o => @l -> @r -> @o.


12 changes: 12 additions & 0 deletions examples/failing/InstanceChainSkolemUnknownMatch.purs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
-- @shouldFailWith NoInstanceFound
module InstanceChainSkolemUnknownMatch where

class Same l r o | l r -> o
instance sameY :: Same t t @"Y" else instance sameN :: Same l r @"N"
same :: forall l r o. Same l r o => l -> r -> @o
same _ _ = @o

-- shouldn't discard sameY as Apart
example :: forall t. @t -> @_
example _ = same @t @Int

70 changes: 38 additions & 32 deletions src/Language/PureScript/TypeChecker/Entailment.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,13 +138,15 @@ data Matched t
= Match t
| Apart
| Unknown
deriving (Eq, Show)
deriving (Eq, Show, Functor)

bothMatched :: Matched () -> Matched () -> Matched ()
bothMatched (Match _) (Match _) = Match ()
bothMatched Unknown r = r
bothMatched l Unknown = l
bothMatched _ _ = Apart
instance Monoid t => Monoid (Matched t) where
mempty = Match mempty

mappend (Match l) (Match r) = Match (l <> r)
mappend Apart _ = Apart
mappend _ Apart = Apart
mappend _ _ = Unknown

-- | Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
-- return a type class dictionary reference.
Expand Down Expand Up @@ -457,7 +459,7 @@ matches deps TypeClassDictionaryInScope{..} tys =
else -- Verify that any repeated type variables are unifiable
let determinedSet = foldMap (S.fromList . fdDetermined) deps
solved = map snd . filter ((`S.notMember` determinedSet) . fst) $ zipWith (\(_, ts) i -> (i, ts)) matched [0..]
in maybe Apart Match $ verifySubstitution (M.unionsWith (++) solved)
in verifySubstitution (M.unionsWith (++) solved)
where
-- | Find the closure of a set of functional dependencies.
covers :: [(Matched (), subst)] -> Bool
Expand Down Expand Up @@ -518,42 +520,46 @@ matches deps TypeClassDictionaryInScope{..} tys =
typeHeadsAreEqual (TUnknown _) _ = (Unknown, M.empty)
typeHeadsAreEqual _ _ = (Apart, M.empty)


both :: (Matched (), Matching [Type]) -> (Matched (), Matching [Type]) -> (Matched (), Matching [Type])
both (b1, m1) (b2, m2) = (bothMatched b1 b2, M.unionWith (++) m1 m2)
both (b1, m1) (b2, m2) = (b1 <> b2, M.unionWith (++) m1 m2)

-- Ensure that a substitution is valid
verifySubstitution :: Matching [Type] -> Maybe (Matching [Type])
verifySubstitution = traverse meet where
meet ts | pairwiseAll typesAreEqual ts = Just ts
| otherwise = Nothing
verifySubstitution :: Matching [Type] -> Matched (Matching [Type])
verifySubstitution mts = foldMap meet mts $> mts where

@paf31 paf31 Oct 20, 2017

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is nice :)

meet = pairwiseAll typesAreEqual

-- Note that unknowns are only allowed to unify if they came from a type
-- which was _not_ solved, i.e. one which was inferred by a functional
-- dependency.
typesAreEqual :: Type -> Type -> Bool
typesAreEqual :: Type -> Type -> Matched ()
typesAreEqual (KindedType t1 _) t2 = typesAreEqual t1 t2
typesAreEqual t1 (KindedType t2 _) = typesAreEqual t1 t2
typesAreEqual (TUnknown u1) (TUnknown u2) | u1 == u2 = True
typesAreEqual (Skolem _ s1 _ _) (Skolem _ s2 _ _) = s1 == s2
typesAreEqual (TypeVar v1) (TypeVar v2) = v1 == v2
typesAreEqual (TypeLevelString s1) (TypeLevelString s2) = s1 == s2
typesAreEqual (TypeConstructor c1) (TypeConstructor c2) = c1 == c2
typesAreEqual (TypeApp h1 t1) (TypeApp h2 t2) = typesAreEqual h1 h2 && typesAreEqual t1 t2
typesAreEqual (TUnknown u1) (TUnknown u2) | u1 == u2 = Match ()
typesAreEqual (Skolem _ s1 _ _) (Skolem _ s2 _ _) | s1 == s2 = Match ()
typesAreEqual (Skolem _ _ _ _) _ = Unknown
typesAreEqual _ (Skolem _ _ _ _) = Unknown
typesAreEqual (TypeVar v1) (TypeVar v2) | v1 == v2 = Match ()
typesAreEqual (TypeLevelString s1) (TypeLevelString s2) | s1 == s2 = Match ()
typesAreEqual (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Match ()
typesAreEqual (TypeApp h1 t1) (TypeApp h2 t2) = typesAreEqual h1 h2 <> typesAreEqual t1 t2
typesAreEqual (ProxyType t1) (ProxyType t2) = typesAreEqual t1 t2
typesAreEqual REmpty REmpty = True
typesAreEqual REmpty REmpty = Match ()
typesAreEqual r1 r2 | isRCons r1 || isRCons r2 =
let (common, rest) = alignRowsWith typesAreEqual r1 r2
in and common && uncurry go rest
in fold common <> uncurry go rest
where
go :: ([(Label, Type)], Type) -> ([(Label, Type)], Type) -> Bool
go :: ([(Label, Type)], Type) -> ([(Label, Type)], Type) -> Matched ()
go (l, KindedType t1 _) (r, t2) = go (l, t1) (r, t2)
go (l, t1) (r, KindedType t2 _) = go (l, t1) (r, t2)
go ([], TUnknown u1) ([], TUnknown u2) | u1 == u2 = True
go ([], Skolem _ s1 _ _) ([], Skolem _ s2 _ _) = s1 == s2
go ([], REmpty) ([], REmpty) = True
go ([], TypeVar v1) ([], TypeVar v2) = v1 == v2
go _ _ = False
typesAreEqual _ _ = False
go ([], TUnknown u1) ([], TUnknown u2) | u1 == u2 = Match ()
go ([], Skolem _ s1 _ _) ([], Skolem _ s2 _ _) | s1 == s2 = Match ()
go ([], Skolem _ _ _ _) _ = Unknown
go _ ([], Skolem _ _ _ _) = Unknown
go ([], REmpty) ([], REmpty) = Match ()
go ([], TypeVar v1) ([], TypeVar v2) | v1 == v2 = Match ()
go _ _ = Apart
typesAreEqual _ _ = Apart

isRCons :: Type -> Bool
isRCons RCons{} = True
Expand Down Expand Up @@ -585,10 +591,10 @@ mkContext = foldr combineContexts M.empty . map fromDict where
fromDict d = M.singleton Nothing (M.singleton (tcdClassName d) (M.singleton (tcdValue d) d))

-- | Check all pairs of values in a list match a predicate
pairwiseAll :: (a -> a -> Bool) -> [a] -> Bool
pairwiseAll _ [] = True
pairwiseAll _ [_] = True
pairwiseAll p (x : xs) = all (p x) xs && pairwiseAll p xs
pairwiseAll :: Monoid m => (a -> a -> m) -> [a] -> m
pairwiseAll _ [] = mempty
pairwiseAll _ [_] = mempty
pairwiseAll p (x : xs) = foldMap (p x) xs <> pairwiseAll p xs

-- | Check any pair of values in a list match a predicate
pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool
Expand Down