X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcCanonical.lhs;h=88414d964fb5da4184ab3351f7b0bccec401708e;hb=a40f2735958055f7ff94e5df73e710044aa63b2c;hp=f834a4c3285d69944798d3d6dcf33290dce1a90c;hpb=67ed735fab12c12a1d48878d7bda33588c67fb78;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index f834a4c..88414d9 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -397,14 +397,6 @@ in Haskell are always
       same type from different type arguments.
 
 
-Note [Kinding] 
-~~~~~~~~~~~~~~
-The canonicalizer assumes that it's provided with well-kinded equalities
-as wanted or given, that is LHS kind and the RHS kind agree, modulo subkinding.
-
-Both canonicalization and interaction solving must preserve this invariant. 
-DV: TODO TODO: Check! 
-
 Note [Canonical ordering for equality constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Implemented as (<+=) below:
@@ -536,21 +528,23 @@ reOrient (FunCls {})   (VarCls tv2)   = isMetaTyVar tv2
   -- meta type variable is the RHS of a function equality
 reOrient (FunCls {}) _                = False   -- Fun/Other on rhs
 
-
-reOrient (VarCls tv1) (FunCls {}) = not (isMetaTyVar tv1)
+reOrient (VarCls tv1) (FunCls {})   = not (isMetaTyVar tv1)
 reOrient (VarCls {})  (OtherCls {}) = False
+reOrient (VarCls {})  (VarCls {})   = False 
 
+{- 
 -- Variables-variables are oriented according to their kind 
--- so that the invariant of CTyEqCan has the best chance of
+-- so that the following property has the best chance of
 -- holding:   tv ~ xi
 --   * If tv is a MetaTyVar, then typeKind xi <: typeKind tv 
 --              a skolem,    then typeKind xi =  typeKind tv 
-reOrient (VarCls tv1) (VarCls tv2)
+
   | k1 `eqKind` k2 = False
   | otherwise      = k1 `isSubKind` k2 
   where
     k1 = tyVarKind tv1
     k2 = tyVarKind tv2
+-} 
 
 ------------------
 canEqLeaf :: CtFlavor -> CoVar 
@@ -582,9 +576,10 @@ canEqLeafOriented :: CtFlavor -> CoVar
                   -> TypeClassifier -> TcType -> TcS CanonicalCts 
 -- First argument is not OtherCls
 canEqLeafOriented fl cv cls1@(FunCls fn tys) s2 
-  | not (kindAppResult (tyConKind fn) tys `eqKind` typeKind s2 )
-  = do { kindErrorTcS fl (unClassify cls1) s2
-       ; return emptyCCan }
+  | let k1 = kindAppResult (tyConKind fn) tys, 
+    let k2 = typeKind s2, 
+    isGiven fl && not (k1 `eqKind` k2)   -- Establish the kind invariant for CFunEqCan
+  = kindErrorTcS fl (unClassify cls1) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract
   | otherwise 
   = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
     do { (xis1,ccs1) <- flattenMany fl tys -- flatten type function arguments
@@ -599,10 +594,8 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys) s2
 -- Otherwise, we have a variable on the left, so we flatten the RHS
 -- and then do an occurs check.
 canEqLeafOriented fl cv (VarCls tv) s2 
-  | not (k1 `eqKind` k2 || (isMetaTyVar tv && k2 `isSubKind` k1))
-      -- Establish the kind invariant for CTyEqCan
-  = do { kindErrorTcS fl (mkTyVarTy tv) s2
-       ; return emptyCCan }
+  | isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CTyEqCan
+  = kindErrorTcS fl (mkTyVarTy tv) s2  -- Eagerly fails, see Note [Kind errors] in TcInteract
 
   | otherwise
   = do { (xi2,ccs2) <- flatten fl s2      -- flatten RHS