[commit: ghc] wip/rae-new-coercible: Solve reflexive repr eqs by reflexivity, even if they're AppTy's. (59d415f)

[git at git.haskell.org]

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

On branch  : wip/rae-new-coercible
Link       : http://ghc.haskell.org/trac/ghc/changeset/59d415fc0c53328635729bd521c310e96b3e2bc0/ghc

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

commit 59d415fc0c53328635729bd521c310e96b3e2bc0
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Mon Dec 1 15:08:29 2014 -0500

    Solve reflexive repr eqs by reflexivity, even if they're AppTy's.


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

59d415fc0c53328635729bd521c310e96b3e2bc0
 compiler/typecheck/TcCanonical.lhs | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 2ee122f..19b9975 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -555,6 +555,11 @@ can_eq_flat_app ev eq_rel swapped s1 t1 ps_ty1 ty2 ps_ty2
   | NomEq <- eq_rel
   , Just (s2,t2) <- tcSplitAppTy_maybe ty2
   = unSwap swapped decompose_it (s1,t1) (s2,t2)
+  | mkAppTy s1 t1 `eqType` ty2  -- this check is necessary for representational
+                                -- equalities, where we might be unable to
+                                -- decompose a reflexive constraint, like
+                                -- Coercible (f a) (f a)
+  = canEqReflexive ev eq_rel ty2
   | otherwise
   = unSwap swapped (canEqFailure ev eq_rel) ps_ty1 ps_ty2
   where
@@ -609,10 +614,7 @@ can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
                  ; stopWith ev "unwrapping newtypes blew stack" }
          else do
        { if ty1 `eqType` ty2   -- See Note [Eager reflexivity check]
-         then do { when (isWanted ev) $
-                   setEvBind (ctev_evar ev) (EvCoercion $
-                                             mkTcReflCo Representational ty1)
-                 ; stopWith ev "Eager reflexivity check before newtype reduction" }
+         then canEqReflexive ev ReprEq ty1
          else do
        { markDataConsAsUsed rdr_env (tyConAppTyCon ty1)
        ; mb_ct <- rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2
@@ -1009,6 +1011,17 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 co2
       =  (isSigTyVar tv1                 && not (isSigTyVar tv2))
       || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
 
+-- | Solve a reflexive equality constraint
+canEqReflexive :: CtEvidence    -- ty ~ ty
+               -> EqRel
+               -> TcType        -- ty
+               -> TcS (StopOrContinue Ct)   -- always Stop
+canEqReflexive ev eq_rel ty
+  = do { when (isWanted ev) $
+         setEvBind (ctev_evar ev) (EvCoercion $
+                                   mkTcReflCo (eqRelRole eq_rel) ty)
+       ; stopWith ev "Solved by reflexivity" }
+
 incompatibleKind :: CtEvidence         -- t1~t2
                  -> TcType -> TcKind
                  -> TcType -> TcKind   -- s1~s2, flattened and zonked