X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcCanonical.lhs;h=d72fae40833234ad6b3a6f9943ed0a83e8508852;hb=2207ce8cdc4c33838f77f285c7dd4f7c75dbae1c;hp=e0c85202b90b90c8deff4070617ceae27f001608;hpb=d2ce0f52d42edf32bb9f13796e6ba6edba8bd516;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index e0c8520..d72fae4 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -1,6 +1,7 @@
 \begin{code}
 module TcCanonical(
-    mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck 
+    mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, 
+    canEq
  ) where
 
 #include "HsVersions.h"
@@ -258,6 +259,31 @@ canEq fl cv ty1 (TyConApp fn tys)
   | isSynFamilyTyCon fn, length tys == tyConArity fn
   = canEqLeaf fl cv (classify ty1) (FunCls fn tys) 
 
+canEq fl cv s1 s2
+  | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1, 
+    Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
+  = do { (v1,v2,v3) <- if isWanted fl then 
+                         do { v1 <- newWantedCoVar t1a t2a
+                            ; v2 <- newWantedCoVar t1b t2b 
+                            ; v3 <- newWantedCoVar t1c t2c 
+                            ; let res_co = mkCoPredCo (mkCoVarCoercion v1) 
+                                                      (mkCoVarCoercion v2) (mkCoVarCoercion v3)
+                            ; setWantedCoBind cv res_co
+                            ; return (v1,v2,v3) }
+                       else let co_orig = mkCoVarCoercion cv 
+                                coa = mkCsel1Coercion co_orig
+                                cob = mkCsel2Coercion co_orig
+                                coc = mkCselRCoercion co_orig
+                            in do { v1 <- newGivOrDerCoVar t1a t2a coa
+                                  ; v2 <- newGivOrDerCoVar t1b t2b cob
+                                  ; v3 <- newGivOrDerCoVar t1c t2c coc 
+                                  ; return (v1,v2,v3) }
+       ; cc1 <- canEq fl v1 t1a t2a 
+       ; cc2 <- canEq fl v2 t1b t2b 
+       ; cc3 <- canEq fl v3 t1c t2c 
+       ; return (cc1 `andCCan` cc2 `andCCan` cc3) }
+
+
 -- Split up an equality between function types into two equalities.
 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
   = do { (argv, resv) <- 
@@ -275,6 +301,34 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
        ; cc2 <- canEq fl resv t1 t2
        ; return (cc1 `andCCan` cc2) }
 
+canEq fl cv (PredTy p1) (PredTy p2) = canEqPred p1 p2 
+  where canEqPred (IParam n1 t1) (IParam n2 t2) 
+          | n1 == n2 
+          = if isWanted fl then 
+                do { v <- newWantedCoVar t1 t2 
+                   ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
+                   ; canEq fl v t1 t2 } 
+            else return emptyCCan -- DV: How to decompose given IP coercions? 
+
+        canEqPred (ClassP c1 tys1) (ClassP c2 tys2) 
+          | c1 == c2 
+          = if isWanted fl then 
+               do { vs <- zipWithM newWantedCoVar tys1 tys2 
+                  ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) 
+                  ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
+                  }
+            else return emptyCCan 
+          -- How to decompose given dictionary (and implicit parameter) coercions? 
+          -- You may think that the following is right: 
+          --    let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) 
+          --    in  zipWith3M newGivOrDerCoVar tys1 tys2 cos
+          -- But this assumes that the coercion is a type constructor-based 
+          -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose
+          -- to not decompose these coercions. We have to get back to this 
+          -- when we clean up the Coercion API.
+
+        canEqPred p1 p2 = misMatchErrorTcS fl (mkPredTy p1) (mkPredTy p2) 
+
 
 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
   | isAlgTyCon tc1 && isAlgTyCon tc2
@@ -311,9 +365,10 @@ canEq fl cv ty1 ty2
          ; cc2 <- canEq fl cv2 t1 t2 
          ; return (cc1 `andCCan` cc2) } 
 
-canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) 
- | Wanted {} <- fl 
- = misMatchErrorTcS fl s1 s2
+canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {})  
+ | tcIsForAllTy s1, tcIsForAllTy s2, 
+   Wanted {} <- fl 
+ = misMatchErrorTcS fl s1 s2 
  | otherwise 
  = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
       ; return emptyCCan }
@@ -321,9 +376,10 @@ canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {})
 -- Finally expand any type synonym applications.
 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
-
 canEq fl _ ty1 ty2 
   = misMatchErrorTcS fl ty1 ty2
+
+
 \end{code}
 
 Note [Equality between type applications]
@@ -341,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:
@@ -480,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 
@@ -526,8 +576,11 @@ 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 )
-  = kindErrorTcS fl (unClassify cls1) s2
+  | let k1 = kindAppResult (tyConKind fn) tys, 
+    let k2 = typeKind s2, 
+    isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CFunEqCan
+  = do { kindErrorTcS fl (unClassify cls1) s2
+       ; return emptyCCan }
   | otherwise 
   = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
     do { (xis1,ccs1) <- flattenMany fl tys -- flatten type function arguments
@@ -542,9 +595,9 @@ 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
-  = kindErrorTcS fl (mkTyVarTy tv) s2
+  | isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CTyEqCan
+  = do { kindErrorTcS fl (mkTyVarTy tv) s2
+       ; return emptyCCan }
 
   | otherwise
   = do { (xi2,ccs2) <- flatten fl s2      -- flatten RHS