X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=d1ea6c0886887350fa8b1114846281999c2bcda5;hb=27286cf2ce6733cbbf008972c6bea30ea2e562ee;hp=b067d99ebebe674c8b0d3d677812b14506fa2031;hpb=dcba7784a1af5fd0c054031c49fe159d69af4f86;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index b067d99..d1ea6c0 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -1088,7 +1088,7 @@ uTysOuter :: InBox -> TcType    -- ty1 is the *actual*   type
           -> TcM CoercionI
 -- We've just pushed a context describing ty1,ty2
 uTysOuter nb1 ty1 nb2 ty2
-        = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+        = do { traceTc (text "uTysOuter" <+> sep [ppr ty1, ppr ty2])
              ; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
 
 uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI
@@ -1099,14 +1099,19 @@ uTys nb1 ty1 nb2 ty2
 
 
 --------------
-uTys_s :: InBox -> [TcType]     -- tys1 are the *actual*   types
+uTys_s :: Outer		
+       -> InBox -> [TcType]     -- tys1 are the *actual*   types
        -> InBox -> [TcType]     -- tys2 are the *expected* types
        -> TcM [CoercionI]
-uTys_s _   []         _   []         = return []
-uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
-                                          ; cois <- uTys_s nb1 tys1 nb2 tys2
-                                          ; return (coi:cois) }
-uTys_s _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!"
+uTys_s outer nb1 tys1 nb2 tys2
+  = go tys1 tys2
+  where
+    go []         []         = return []
+    go (ty1:tys1) (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
+                                  ; cois <- go tys1 tys2
+                                  ; return (coi:cois) }
+    go _ _ = unifyMisMatch outer
+       -- See Note [Mismatched type lists and application decomposition]
 
 --------------
 u_tys :: Outer
@@ -1169,8 +1174,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
 
              ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
              { unless (equalLength theta1 theta2) (bale_out outer)
-             ; _cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
-             ; traceTc (text "TOMDO!")
+             ; cois <- uPreds outer nb1 theta1 nb2 theta2
              ; coi <- uTys nb1 tau1 nb2 tau2
 
                 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
@@ -1185,7 +1189,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
                 -- This check comes last, because the error message is
                 -- extremely unhelpful.
              ; when (nb1 && nb2) (notMonoType ty1)
-             ; return coi
+             ; let mk_fun (pred, coi_pred) (ty, coi) 
+                       = (mkFunTy pred_ty ty, mkFunTyCoI pred_ty coi_pred ty coi)
+                       where
+                         pred_ty = mkPredTy pred
+             ; return (foldr mkForAllTyCoI 
+                             (snd (foldr mk_fun (tau1,coi) (theta1 `zip` cois)))
+                             tvs)
              }}
       where
         (tvs1, body1) = tcSplitForAllTys ty1
@@ -1196,14 +1206,16 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
         = uPred outer nb1 p1 nb2 p2
 
         -- Non-synonym type constructors must match
-    go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
+    go outer _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
       | con1 == con2 && not (isOpenSynTyCon con1)
-      = do { cois <- uTys_s nb1 tys1 nb2 tys2
+      = do { traceTc (text "utys1" <+> ppr con1 <+> (ppr tys1 $$ ppr tys2))
+           ; cois <- uTys_s outer nb1 tys1 nb2 tys2
            ; return $ mkTyConAppCoI con1 tys1 cois
            }
         -- Family synonyms See Note [TyCon app]
       | con1 == con2 && identicalOpenSynTyConApp
-      = do { cois <- uTys_s nb1 tys1' nb2 tys2'
+      = do { traceTc (text "utys2" <+> ppr con1 <+> (ppr tys1' $$ ppr tys2'))
+           ; cois <- uTys_s outer nb1 tys1' nb2 tys2'
            ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
            }
       where
@@ -1224,9 +1236,10 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
         -- NB: we've already dealt with type variables and Notes,
         -- so if one type is an App the other one jolly well better be too
+        -- See Note [Mismatched type lists and application decomposition]
     go outer _ (AppTy s1 t1) _ ty2
       | Just (s2,t2) <- tcSplitAppTy_maybe ty2
-      = do { coi_s <- go outer s1 s1 s2 s2      -- NB recurse into go
+      = do { coi_s <- go outer s1 s1 s2 s2      -- NB recurse into go...
            ; coi_t <- uTys nb1 t1 nb2 t2        -- See Note [Unifying AppTy]
            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
 
@@ -1271,15 +1284,14 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
 ----------
 uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
 uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)
-  | n1 == n2 =
-        do { coi <- uTys nb1 t1 nb2 t2
-           ; return $ mkIParamPredCoI n1 coi
-           }
-uPred _ nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
-  | c1 == c2 =
-        do { cois <- uTys_s nb1 tys1 nb2 tys2           -- Guaranteed equal lengths because the kinds check
-           ; return $ mkClassPPredCoI c1 tys1 cois
-           }
+  | n1 == n2
+  = do { coi <- uTys nb1 t1 nb2 t2
+       ; return $ mkIParamPredCoI n1 coi }
+uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
+  | c1 == c2
+  = do { traceTc (text "utys3" <+> ppr c1 <+> (ppr tys2 $$ ppr tys2))
+       ; cois <- uTys_s outer nb1 tys1 nb2 tys2
+       ; return $ mkClassPPredCoI c1 tys1 cois }
 uPred outer _ _ _ _ = unifyMisMatch outer
 
 uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType]
@@ -1293,15 +1305,23 @@ uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
 uPreds _ _ _ _ _ = panic "uPreds"
 \end{code}
 
-Note [TyCon app]
-~~~~~~~~~~~~~~~~
-When we find two TyConApps, the argument lists are guaranteed equal
-length.  Reason: intially the kinds of the two types to be unified is
-the same. The only way it can become not the same is when unifying two
-AppTys (f1 a1)~(f2 a2).  In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app).  If we unify f1~f2 first,
-which we do, that ensures that f1,f2 have the same kind; and that
-means a1,a2 have the same kind.  And now the argument repeats.
+Note [Mismatched type lists and application decomposition]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we find two TyConApps, you might think that the argument lists 
+are guaranteed equal length.  But they aren't. Consider matching
+	w (T x) ~ Foo (T x y)
+We do match (w ~ Foo) first, but in some circumstances we simply create
+a deferred constraint; and then go ahead and match (T x ~ T x y).
+This came up in Trac #3950.
+
+So either 
+   (a) either we must check for identical argument kinds 
+       when decomposing applications,
+  
+   (b) or we must be prepared for ill-kinded unification sub-problems
+
+Currently we adopt (b) since it seems more robust -- no need to maintain
+a global invariant.
 
 Note [OpenSynTyCon app]
 ~~~~~~~~~~~~~~~~~~~~~~~