X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=7bb8680861c023571505e274ba9e7a19100131c7;hb=1e436f2bb208a6c990743afaf17b7c2a93c31742;hp=c7fac2d1ce918444b9d3f5d8e9989e324d4f57cd;hpb=296058a1cafa80dec0b3f998348bce7c65f668b0;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index c7fac2d..7bb8680 100644
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -38,7 +38,6 @@ import Bag
 import Outputable
 import SrcLoc	( Located(..) )
 import Maybes
-import MonadUtils
 import FastString
 
 -- standard
@@ -662,7 +661,7 @@ checkOrientation ty1 ty2 co inst
       -- NB: Special cased for efficiency - could be handled as type application
     go (TyConApp con1 args1) (TyConApp con2 args2)
       |  con1 == con2
-      && not (isOpenSynTyCon con1)   -- don't match family synonym apps
+      && isInjectiveTyCon con1   -- don't match family synonym apps
       = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
            ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
                      args1 args2 co_args
@@ -795,18 +794,19 @@ flattenType inst ty = go ty
                      thisRewriteFam : concat args_eqss)
            }
 
-      -- data constructor application => flatten subtypes
+      -- datatype constructor application => flatten subtypes
       -- NB: Special cased for efficiency - could be handled as type application
     go ty@(TyConApp con args)
       | not (isOpenSynTyCon con)   -- don't match oversaturated family apps
       = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
-           ; if null args_eqss
+           ; let args_eqs = concat args_eqss
+           ; if null args_eqs
              then     -- unchanged, keep the old type with folded synonyms
                return (ty, ty, [])
              else 
                return (mkTyConApp con args', 
                        mkTyConApp con cargs,
-                       concat args_eqss)
+                       args_eqs)
            }
 
       -- function type => flatten subtypes
@@ -849,9 +849,32 @@ flattenType inst ty = go ty
       | otherwise
       = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
 
-      -- we should never see a predicate type
-    go (PredTy _)
-      = panic "TcTyFuns.flattenType: unexpected PredType"
+      -- predicate type => handle like a datatype constructor application
+    go (PredTy (ClassP cls tys))
+      = do { (tys', ctys, tys_eqss) <- mapAndUnzip3M go tys
+           ; let tys_eqs = concat tys_eqss
+           ; if null tys_eqs
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [])
+             else 
+               return (PredTy (ClassP cls tys'), 
+                       PredTy (ClassP cls ctys),
+                       tys_eqs)
+           }
+
+      -- implicit parameter => flatten subtype
+    go ty@(PredTy (IParam ipn ity))
+      = do { (ity', co, eqs) <- go ity
+           ; if null eqs 
+             then return (ty, ty, []) 
+             else return (PredTy (IParam ipn ity'),
+                          PredTy (IParam ipn co),
+                          eqs)
+           }
+
+      -- we should never see a equality
+    go (PredTy (EqPred _ _))
+      = panic "TcTyFuns.flattenType: malformed type"
 
     go _ = panic "TcTyFuns: suppress bogus warning"
 
@@ -1576,10 +1599,9 @@ somethingdifferent message.
 eqInstMisMatch :: Inst -> TcM a
 eqInstMisMatch inst
   = ASSERT( isEqInst inst )
-    setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
+    setInstCtxt (instLoc inst) $ failWithMisMatch ty_act ty_exp
   where
     (ty_act, ty_exp) = eqInstTys inst
-    InstLoc _ _ ctxt = instLoc   inst
 
 -----------------------
 failWithMisMatch :: TcType -> TcType -> TcM a
@@ -1600,11 +1622,21 @@ misMatchMsg env0 (ty_act, ty_exp)
         msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp, 
 			nest 7 $
                               ptext (sLit "against inferred type") <+> pp_act],
-		   nest 2 (extra_exp $$ extra_act)]
+		   nest 2 (extra_exp $$ extra_act),
+		   nest 2 (vcat (map pp_open_tc (nub open_tcs)))]
+		   	-- See Note [Non-injective type functions]
     in
     (env2, msg)
 
   where
+    open_tcs = [tc | TyConApp tc _ <- [ty_act, ty_exp]
+                   , isOpenTyCon tc ]
+    pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc) 
+    	       	    <+> ptext (sLit "is a type function") <> pp_inj
+	where
+          pp_inj | isInjectiveTyCon tc = empty
+                 | otherwise = ptext (sLit (", and may not be injective"))
+
     ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
     ppr_ty env ty
       = let (env1, tidy_ty) = tidyOpenType env ty
@@ -1623,6 +1655,24 @@ misMatchMsg env0 (ty_act, ty_exp)
     ppr_extra env _ty = (env, empty)		-- Normal case
 \end{code}
 
+Note [Non-injective type functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's very confusing to get a message like
+     Couldn't match expected type `Depend s'
+            against inferred type `Depend s1'
+so pp_open_tc adds:
+       NB: `Depend' is type function, and hence may not be injective
+
+Currently we add this independently for each argument, so we also get
+     Couldn't match expected type `a'
+            against inferred type `Dual (Dual a)'
+       NB: `Dual' is a (non-injective) type function
+which is arguably redundant.  But on the other hand, it's probably
+a good idea for the programmer to know the error involves type functions
+so I've left it in for now.  The obvious alternative is to only add
+this NB in the case of matching (T ...) ~ (T ...). 
+     
+
 Warn of loopy local equalities that were dropped.
 
 \begin{code}