[commit: ghc] master: Eliminate (given) flatten-skolems in favour of user type variables (db07129)

[Simon Peyton Jones]

Repository : http://darcs.haskell.org/ghc.git/

On branch  : master

https://github.com/ghc/ghc/commit/db07129cfb13a856f31276c76e9e00924835b18e

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

commit db07129cfb13a856f31276c76e9e00924835b18e
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu May 2 17:14:23 2013 +0100

    Eliminate (given) flatten-skolems in favour of user type variables
    
    See Note [Eliminate flat-skols].  IT wasn't exactly wrong before
    the the error messages are deeply strange.

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

 compiler/typecheck/TcCanonical.lhs | 23 +++++++++++++++++++++--
 compiler/typecheck/TcType.lhs      | 10 ++++++++--
 2 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 15a7274..db1c5a0 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -1015,8 +1015,9 @@ reOrient (FunCls {}) _      = False             -- Fun/Other on rhs
 reOrient (VarCls {})   (FunCls {})           = True 
 reOrient (VarCls {})   (OtherCls {})         = False
 reOrient (VarCls tv1)  (VarCls tv2)  
-  | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
-  | otherwise                                = False 
+  | isMetaTyVar     tv2 && not (isMetaTyVar tv1)      = True 
+  | isFlatSkolTyVar tv2 && not (isFlatSkolTyVar tv1)  = True  -- Note [Eliminate flat-skols]
+  | otherwise                                         = False 
   -- Just for efficiency, see CTyEqCan invariants 
 
 ------------------
@@ -1184,6 +1185,24 @@ mkHdEqPred t2 co1 co2 = mkTcTyConAppCo eqTyCon [mkTcReflCo (defaultKind (typeKin
    -- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I truly hate this (DV)
 \end{code}
 
+Note [Eliminate flat-skols]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have  [G] Num (F [a])
+then we flatten to
+     [G] Num fsk
+     [G] F [a] ~ fsk
+where fsk is a flatten-skolem (FlatSkol). Suppose we have
+      type instance F [a] = a
+then we'll reduce the second constraint to
+     [G] a ~ fsk
+and then replace all uses of 'a' with fsk.  That's bad because
+in error messages intead of saying 'a' we'll say (F [a]).  In all
+places, including those where the programmer wrote 'a' in the first
+place.  Very confusing!  See Trac #7862.
+
+Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
+the fsk.
+
 Note [Equalities with incompatible kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 77f7de6..a3d3156 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -37,7 +37,7 @@ module TcType (
   TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
   MetaDetails(Flexi, Indirect), MetaInfo(..), 
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
-  isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
+  isSigTyVar, isOverlappableTyVar,  isTyConableTyVar, isFlatSkolTyVar,
   isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
   isFlexi, isIndirect, isRuntimeUnkSkol,
   isTypeVar, isKindVar, 
@@ -613,7 +613,7 @@ isImmutableTyVar tv
   | otherwise    = True
 
 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
-  isMetaTyVar, isAmbiguousTyVar :: TcTyVar -> Bool 
+  isMetaTyVar, isAmbiguousTyVar, isFlatSkolTyVar :: TcTyVar -> Bool 
 
 isTyConableTyVar tv	
 	-- True of a meta-type variable that can be filled in 
@@ -624,6 +624,12 @@ isTyConableTyVar tv
 	MetaTv { mtv_info = SigTv } -> False
 	_                           -> True
 	
+isFlatSkolTyVar tv
+  = ASSERT2( isTcTyVar tv, ppr tv )
+    case tcTyVarDetails tv of
+        FlatSkol {} -> True
+        _           -> False
+
 isSkolemTyVar tv 
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of