diff options
| -rw-r--r-- | compiler/typecheck/TcFlatten.hs | 5 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 20 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/T15144.hs | 18 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/all.T | 1 |
4 files changed, 41 insertions, 3 deletions
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 45435a145e..e2244a99e6 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -2015,7 +2015,10 @@ unflattenWanteds tv_eqs funeqs unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest - | isFmvTyVar tv -- Previously these fmvs were untouchable, + + | NomEq <- eq_rel -- See Note [Do not unify representational equalities] + -- in TcInteract + , isFmvTyVar tv -- Previously these fmvs were untouchable, -- but now they are touchable -- NB: unlike unflattenFmv, filling a fmv here /does/ -- bump the unification count; it is "improvement" diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index c71a01aa6c..7f85d6b055 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -1600,8 +1600,8 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv ; stopWith ev "Solved from inert" } - | ReprEq <- eq_rel -- We never solve representational - = unsolved_inert -- equalities by unification + | ReprEq <- eq_rel -- See Note [Do not unify representational equalities] + = unsolved_inert | isGiven ev -- See Note [Touchables and givens] = unsolved_inert @@ -1672,6 +1672,22 @@ See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding double unifications is the main reason we disallow touchable unification variables as RHS of type family equations: F xis ~ alpha. +Note [Do not unify representational equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider [W] alpha ~R# b +where alpha is touchable. Should we unify alpha := b? + +Certainly not! Unifying forces alpha and be to be the same; but they +only need to be representationally equal types. + +For example, we might have another constraint [W] alpha ~# N b +where + newtype N b = MkN b +and we want to get alpha := N b. + +See also Trac #15144, which was caused by unifying a representational +equality (in the unflattener). + ************************************************************************ * * diff --git a/testsuite/tests/indexed-types/should_compile/T15144.hs b/testsuite/tests/indexed-types/should_compile/T15144.hs new file mode 100644 index 0000000000..c6f0856184 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15144.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} +module T15144 where + +import Data.Coerce +import Data.Proxy + +type family F x + +f :: Coercible (F a) b => Proxy a -> F a -> b +f _ = coerce + +-- In #15144, we inferred the less-general type +-- g :: Proxy a -> F a -> F a +g p x = f p x + +h :: Coercible (F a) b => Proxy a -> F a -> b +h p x = g p x diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 6074a3597e..9f0d9b4a8d 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -280,3 +280,4 @@ test('T14237', normal, compile, ['']) test('T14554', normal, compile, ['']) test('T14680', normal, compile, ['']) test('T15057', normal, compile, ['']) +test('T15144', normal, compile, ['']) |