Commit ae292c6d authored by Simon Peyton Jones's avatar Simon Peyton Jones

Do not unify representational equalities

This patch is an easy fix to Trac #15144, which was caused
by accidentally unifying a representational equality in the
unflattener.  (The main code in TcInteract was always careful
not to do so, but I'd missed the test in the unflattener.)

See Note [Do not unify representational equalities]
in TcInteract
parent 5a7c657e
......@@ -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"
......
......@@ -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).
************************************************************************
* *
......
{-# 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
......@@ -280,3 +280,4 @@ test('T14237', normal, compile, [''])
test('T14554', normal, compile, [''])
test('T14680', normal, compile, [''])
test('T15057', normal, compile, [''])
test('T15144', normal, compile, [''])
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