[commit: ghc] ghc-7.8: Flattener preserves synonyms, rewriteEvidence can drop buggy "optimisation" (09062bd)
git at git.haskell.org
git at git.haskell.org
Mon Mar 24 12:04:43 UTC 2014
Repository : ssh://git@git.haskell.org/ghc
On branch : ghc-7.8
Link : http://ghc.haskell.org/trac/ghc/changeset/09062bdf1d0b54f078dd200eb9e04a94b15682b4/ghc
>---------------------------------------------------------------
commit 09062bdf1d0b54f078dd200eb9e04a94b15682b4
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Mar 21 15:37:27 2014 +0000
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.
(cherry picked from commit 6ae678e31a5fdd3b0bd1f8613fe164012bb630f4)
>---------------------------------------------------------------
09062bdf1d0b54f078dd200eb9e04a94b15682b4
compiler/typecheck/TcCanonical.lhs | 23 +++++++++------
compiler/typecheck/TcSMonad.lhs | 31 ++++++++++----------
.../tests/indexed-types/should_compile/T8913.hs | 16 ++++++++++
testsuite/tests/indexed-types/should_compile/all.T | 1 +
.../tests/simplCore/should_compile/simpl017.stderr | 14 +++------
5 files changed, 51 insertions(+), 34 deletions(-)
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index bb0b279..6cd77b1 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -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
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 1cc18d1..0cb7c92 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -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
diff --git a/testsuite/tests/indexed-types/should_compile/T8913.hs b/testsuite/tests/indexed-types/should_compile/T8913.hs
new file mode 100644
index 0000000..062a252
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T8913.hs
@@ -0,0 +1,16 @@
+{-# 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
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 5c156ec..76682ad 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -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, [''])
diff --git a/testsuite/tests/simplCore/should_compile/simpl017.stderr b/testsuite/tests/simplCore/should_compile/simpl017.stderr
index b04dbb4..18b0a69 100644
--- a/testsuite/tests/simplCore/should_compile/simpl017.stderr
+++ b/testsuite/tests/simplCore/should_compile/simpl017.stderr
@@ -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)
More information about the ghc-commits
mailing list