Commit 6ae678e3 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Flattener preserves synonyms, rewriteEvidence can drop buggy "optimisation"

There was a special case in rewriteEvidence, looking like:
  = return (Just (if ctEvPred old_ev `tcEqType` new_pred
                  then old_ev
                  else old_ev { ctev_pred = new_pred }))

But this was wrong: old_pred and new_pred might differ in the kind
of a TyVar occurrence, in which case tcEqType would not notice,
but we really, really want new_pred.  This caused Trac #8913.

I solved this by dropping the whole test, and instead making
the flattener preserve type synonyms. This was easy because
TcEvidence has TcTyConAppCo which (unlike) Coercion, handles
synonyms.
parent 9f9b10f6
......@@ -475,14 +475,6 @@ flatten :: FlattenMode
--
-- Postcondition: Coercion :: Xi ~ TcType
flatten f ctxt ty
| Just ty' <- tcView ty
= do { (xi, co) <- flatten f ctxt ty'
; if xi `tcEqType` ty' then return (ty,co)
else return (xi,co) }
-- Small tweak for better error messages
-- by preserving type synonyms where possible
flatten _ _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
flatten f ctxt (TyVarTy tv)
......@@ -500,7 +492,9 @@ flatten f ctxt (FunTy ty1 ty2)
; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
flatten f ctxt (TyConApp tc tys)
-- For a normal type constructor or data family application,
-- For * a normal data type application
-- * type synonym application See Note [Flattening synonyms]
-- * data family application
-- we just recursively flatten the arguments.
| not (isSynFamilyTyCon tc)
= do { (xis,cos) <- flattenMany f ctxt tys
......@@ -538,6 +532,17 @@ flatten _f ctxt ty@(ForAllTy {})
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
\end{code}
Note [Flattening synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose
type T a = a -> a
and we want to flatten the type (T (F a)). Then we can safely flatten
the (F a) to a skolem, and return (T fsk). We don't need to expand the
synonym. This works because TcTyConAppCo can deal with synonyms
(unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
Not expanding synonyms aggressively improves error messages.
Note [Flattening under a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Under a forall, we
......
......@@ -1724,7 +1724,18 @@ Main purpose: create new evidence for new_pred;
Given Already in inert Nothing
Not Just new_evidence
-}
Note [Rewriting with Refl]
~~~~~~~~~~~~~~~~~~~~~~~~~~
If the coercion is just reflexivity then you may re-use the same
variable. But be careful! Although the coercion is Refl, new_pred
may reflect the result of unification alpha := ty, so new_pred might
not _look_ the same as old_pred, and it's vital to proceed from now on
using new_pred.
The flattener preserves type synonyms, so they should appear in new_pred
as well as in old_pred; that is important for good error messages.
-}
rewriteEvidence (CtDerived { ctev_loc = loc }) new_pred _co
......@@ -1738,15 +1749,8 @@ rewriteEvidence (CtDerived { ctev_loc = loc }) new_pred _co
newDerived loc new_pred
rewriteEvidence old_ev new_pred co
| isTcReflCo co -- If just reflexivity then you may re-use the same variable
= return (Just (if ctEvPred old_ev `tcEqType` new_pred
then old_ev
else old_ev { ctev_pred = new_pred }))
-- Even if the coercion is Refl, it might reflect the result of unification alpha := ty
-- so old_pred and new_pred might not *look* the same, and it's vital to proceed from
-- now on using new_pred.
-- However, if they *do* look the same, we'd prefer to stick with old_pred
-- then retain the old type, so that error messages come out mentioning synonyms
| isTcReflCo co -- See Note [Rewriting with Refl]
= return (Just (old_ev { ctev_pred = new_pred }))
rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm) -- See Note [Bind new Givens immediately]
......@@ -1789,12 +1793,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
= newDerived loc (mkEqPred nlhs nrhs)
| NotSwapped <- swapped
, isTcReflCo lhs_co
, isTcReflCo lhs_co -- See Note [Rewriting with Refl]
, isTcReflCo rhs_co
, let new_pred = mkTcEqPred nlhs nrhs
= return (Just (if ctEvPred old_ev `tcEqType` new_pred
then old_ev
else old_ev { ctev_pred = new_pred }))
= return (Just (old_ev { ctev_pred = new_pred }))
| CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
= do { let new_tm = EvCoercion (lhs_co
......
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
module T8913 where
class GCat f where
gcat :: f p -> Int
cat :: (GCat (MyRep a), MyGeneric a) => a -> Int
cat x = gcat (from x)
class MyGeneric a where
type MyRep a :: * -> *
from :: a -> (MyRep a) p
......@@ -240,3 +240,4 @@ test('ClosedFam2', extra_clean(['ClosedFam2.o-boot', 'ClosedFam2.hi-boot']),
multimod_compile, ['ClosedFam2', '-v0'])
test('T8651', normal, compile, [''])
test('T8889', normal, compile, [''])
test('T8913', normal, compile, [''])
......@@ -12,11 +12,8 @@ simpl017.hs:44:12:
In a stmt of a 'do' block: return f
simpl017.hs:63:5:
Couldn't match type ‘forall v.
[E' RValue (ST s) Int] -> E' v (ST s) Int’
with ‘[E (ST t0) Int] -> E' RValue (ST s) Int’
Expected type: [E (ST t0) Int] -> E (ST s) Int
Actual type: forall v. [E (ST s) Int] -> E' v (ST s) Int
Couldn't match expected type ‘[E (ST t0) Int] -> E (ST s) Int’
with actual type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’
Relevant bindings include
a :: forall v. [E (ST s) Int] -> E' v (ST s) Int
(bound at simpl017.hs:60:5)
......@@ -28,11 +25,8 @@ simpl017.hs:63:5:
In a stmt of a 'do' block: a [one] `plus` a [one]
simpl017.hs:63:19:
Couldn't match type ‘forall v.
[E' RValue (ST s) Int] -> E' v (ST s) Int’
with ‘[E (ST t1) Int] -> E' RValue (ST s) Int’
Expected type: [E (ST t1) Int] -> E (ST s) Int
Actual type: forall v. [E (ST s) Int] -> E' v (ST s) Int
Couldn't match expected type ‘[E (ST t1) Int] -> E (ST s) Int’
with actual type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’
Relevant bindings include
a :: forall v. [E (ST s) Int] -> E' v (ST s) Int
(bound at simpl017.hs:60:5)
......
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