Commit f877d9cc authored by mniip's avatar mniip Committed by Ben Gamari

Move eta-reduced coaxiom compatibility handling quirks into FamInstEnv.

The quirk caused an issue where GHC concluded that 'D' is possibly
unifiable with 'D a' (the two types could have the same kind if D is a
data family).

Test Plan:
Ensure T9371 stays fixed.
Introduce T15704

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: RyanGlScott, rwbarton, carter

GHC Trac Issues: #15704

Differential Revision: https://phabricator.haskell.org/D5206
parent 1c92f193
...@@ -551,13 +551,42 @@ find a branch that matches the target, but then we make sure that the target ...@@ -551,13 +551,42 @@ find a branch that matches the target, but then we make sure that the target
is apart from every previous *incompatible* branch. We don't check the is apart from every previous *incompatible* branch. We don't check the
branches that are compatible with the matching branch, because they are either branches that are compatible with the matching branch, because they are either
irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
Note [Compatibility of eta-reduced axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In newtype instances of data families we eta-reduce the axioms,
See Note [Eta reduction for data family axioms] in TcInstDcls. This means that
we sometimes need to test compatibility of two axioms that were eta-reduced to
different degrees, e.g.:
data family D a b c
newtype instance D a Int c = DInt (Maybe a)
-- D a Int ~ Maybe
-- lhs = [a, Int]
newtype instance D Bool Int Char = DIntChar Float
-- D Bool Int Char ~ Float
-- lhs = [Bool, Int, Char]
These are obviously incompatible. We could detect this by saturating
(eta-expanding) the shorter LHS with fresh tyvars until the lists are of
equal length, but instead we can just remove the tail of the longer list, as
those types will simply unify with the freshly introduced tyvars.
By doing this, in case the LHS are unifiable, the yielded substitution won't
mention the tyvars that appear in the tail we dropped off, and we might try
to test equality RHSes of different kinds, but that's fine since this case
occurs only for data families, where the RHS is a unique tycon and the equality
fails anyway.
-} -}
-- See Note [Compatibility] -- See Note [Compatibility]
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
= case tcUnifyTysFG (const BindMe) lhs1 lhs2 of = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
-- See Note [Compatibility of eta-reduced axioms]
in case tcUnifyTysFG (const BindMe) commonlhs1 commonlhs2 of
SurelyApart -> True SurelyApart -> True
Unifiable subst Unifiable subst
| Type.substTyAddInScope subst rhs1 `eqType` | Type.substTyAddInScope subst rhs1 `eqType`
......
...@@ -344,26 +344,6 @@ If we discover that two types unify if and only if a skolem variable is ...@@ -344,26 +344,6 @@ If we discover that two types unify if and only if a skolem variable is
substituted, we can't properly unify the types. But, that skolem variable substituted, we can't properly unify the types. But, that skolem variable
may later be instantiated with a unifyable type. So, we return maybeApart may later be instantiated with a unifyable type. So, we return maybeApart
in these cases. in these cases.
Note [Lists of different lengths are MaybeApart]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
lengths. The place where we know this can happen is from compatibleBranches in
FamInstEnv, when checking data family instances. Data family instances may be
eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.
We wish to say that
D :: * -> * -> *
axDF1 :: D Int ~ DFInst1
axDF2 :: D Int Bool ~ DFInst2
overlap. If we conclude that lists of different lengths are SurelyApart, then
it will look like these do *not* overlap, causing disaster. See Trac #9371.
In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
which can't tell the difference between MaybeApart and SurelyApart, so those
usages won't notice this design choice.
-} -}
-- | Simple unification of two types; all type variables are bindable -- | Simple unification of two types; all type variables are bindable
...@@ -1044,7 +1024,8 @@ unify_tys env orig_xs orig_ys ...@@ -1044,7 +1024,8 @@ unify_tys env orig_xs orig_ys
-- See Note [Kind coercions in Unify] -- See Note [Kind coercions in Unify]
= do { unify_ty env x y (mkNomReflCo $ typeKind x) = do { unify_ty env x y (mkNomReflCo $ typeKind x)
; go xs ys } ; go xs ys }
go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart] go _ _ = surelyApart
-- Possibly different saturations of a polykinded tycon (See Trac #15704)
--------------------------------- ---------------------------------
uVar :: UMEnv uVar :: UMEnv
......
...@@ -16,7 +16,7 @@ module Util ( ...@@ -16,7 +16,7 @@ module Util (
-- * General list processing -- * General list processing
zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal, zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal,
zipLazy, stretchZipWith, zipWithAndUnzip, zipLazy, stretchZipWith, zipWithAndUnzip, zipAndUnzip,
zipWithLazy, zipWith3Lazy, zipWithLazy, zipWith3Lazy,
...@@ -441,6 +441,15 @@ zipWithAndUnzip f (a:as) (b:bs) ...@@ -441,6 +441,15 @@ zipWithAndUnzip f (a:as) (b:bs)
(r1:rs1, r2:rs2) (r1:rs1, r2:rs2)
zipWithAndUnzip _ _ _ = ([],[]) zipWithAndUnzip _ _ _ = ([],[])
-- | This has the effect of making the two lists have equal length by dropping
-- the tail of the longer one.
zipAndUnzip :: [a] -> [b] -> ([a],[b])
zipAndUnzip (a:as) (b:bs)
= let (rs1, rs2) = zipAndUnzip as bs
in
(a:rs1, b:rs2)
zipAndUnzip _ _ = ([],[])
mapAccumL2 :: (s1 -> s2 -> a -> (s1, s2, b)) -> s1 -> s2 -> [a] -> (s1, s2, [b]) mapAccumL2 :: (s1 -> s2 -> a -> (s1, s2, b)) -> s1 -> s2 -> [a] -> (s1, s2, [b])
mapAccumL2 f s1 s2 xs = (s1', s2', ys) mapAccumL2 f s1 s2 xs = (s1', s2', ys)
where ((s1', s2'), ys) = mapAccumL (\(s1, s2) x -> case f s1 s2 x of where ((s1', s2'), ys) = mapAccumL (\(s1, s2) x -> case f s1 s2 x of
......
{-# LANGUAGE TypeFamilies, PolyKinds #-}
module T15704 where
import Data.Kind
data family D :: k
type family F (a :: k) :: Type
type instance F D = Int
type instance F (D a) = Char
...@@ -294,4 +294,5 @@ test('T15322a', normal, compile_fail, ['']) ...@@ -294,4 +294,5 @@ test('T15322a', normal, compile_fail, [''])
test('T15142', normal, compile, ['']) test('T15142', normal, compile, [''])
test('T15352', normal, compile, ['']) test('T15352', normal, compile, [''])
test('T15664', normal, compile, ['']) test('T15664', normal, compile, [''])
test('T15704', normal, compile, [''])
test('T15711', normal, compile, ['-ddump-types']) test('T15711', normal, compile, ['-ddump-types'])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment