[commit: ghc] master: Flattener preserves synonyms, rewriteEvidence can drop buggy "optimisation" (6ae678e)

git at git.haskell.org git at git.haskell.org
Mon Mar 24 10:27:05 UTC 2014


Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/6ae678e31a5fdd3b0bd1f8613fe164012bb630f4/ghc

>---------------------------------------------------------------

commit 6ae678e31a5fdd3b0bd1f8613fe164012bb630f4
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.


>---------------------------------------------------------------

6ae678e31a5fdd3b0bd1f8613fe164012bb630f4
 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 a906270..3e23756 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 a92bc95..b7faf15 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