Flattener preserves synonyms, rewriteEvidence can drop buggy "optimisation"
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 21 Mar 2014 15:37:27 +0000 (15:37 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 24 Mar 2014 08:28:02 +0000 (08:28 +0000)
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.

compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcSMonad.lhs
testsuite/tests/indexed-types/should_compile/T8913.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/simplCore/should_compile/simpl017.stderr

index a906270..3e23756 100644 (file)
@@ -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
index a92bc95..b7faf15 100644 (file)
@@ -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 (file)
index 0000000..062a252
--- /dev/null
@@ -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
index 5c156ec..76682ad 100644 (file)
@@ -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, [''])
index b04dbb4..18b0a69 100644 (file)
@@ -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)