X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=04e9379e7c0b64d9887197d80774e762f6d22dfd;hb=2e68d0410f319a99f3f36c5e9d9be656ca10dc70;hp=f188af1544ed75bd9afa901a3da6750e9ceeca49;hpb=6d2b0ae3ae3296cb6cdd496cbf85b897c7ce150b;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index f188af1..04e9379 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -28,7 +28,7 @@ module TcUnify (
   -- Holes
   tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, 
   boxyUnify, boxyUnifyList, zapToMonotype,
-  boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
+  boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy,
   wrapFunResCoercion
   ) where
 
@@ -128,7 +128,8 @@ subFunTys error_herald n_pats res_ty thing_inside
 
     loop n args_so_far res_ty
 	| isSigmaTy res_ty 	-- Do this before checking n==0, because we 
-				-- guarantee to return a BoxyRhoType, not a BoxySigmaType
+				-- guarantee to return a BoxyRhoType, not a 
+                                -- BoxySigmaType
 	= do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
 					 loop n args_so_far res_ty'
 	     ; return (gen_fn <.> co_fn, res) }
@@ -142,29 +143,47 @@ subFunTys error_herald n_pats res_ty thing_inside
 	     ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
 	     ; return (co_fn', res) }
 
+        -- Try to normalise synonym families and defer if that's not possible
+    loop n args_so_far ty@(TyConApp tc tys)
+        | isOpenSynTyCon tc
+        = do { (coi1, ty') <- tcNormaliseFamInst ty
+             ; case coi1 of
+	         IdCo   -> defer n args_so_far ty
+                                    -- no progress, but maybe solvable => defer
+                 ACo _  ->          -- progress: so lets try again
+        	   do { (co_fn, res) <- loop n args_so_far ty'
+		      ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res)
+		      }
+             }
+
 	-- res_ty might have a type variable at the head, such as (a b c),
 	-- in which case we must fill in with (->).  Simplest thing to do
 	-- is to use boxyUnify, but we catch failure and generate our own
 	-- error message on failure
     loop n args_so_far res_ty@(AppTy _ _)
 	= do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
-	     ; (_, mb_coi) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
+	     ; (_, mb_coi) <- tryTcErrs $ 
+                                boxyUnify res_ty (FunTy arg_ty' res_ty')
 	     ; if isNothing mb_coi then bale_out args_so_far
-	       else do { case expectJust "subFunTys" mb_coi of
-				IdCo -> return ()
-				ACo co -> traceTc (text "you're dropping a coercion: " <+> ppr co)
-		       ; loop n args_so_far (FunTy arg_ty' res_ty') 
+	       else do { let coi = expectJust "subFunTys" mb_coi
+		       ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty' 
+                                                                   res_ty')
+                       ; return (co_fn <.> coiToHsWrapper coi, res)
 		       }
 	     }
 
-    loop n args_so_far (TyVarTy tv)
+    loop n args_so_far ty@(TyVarTy tv)
         | isTyConableTyVar tv
 	= do { cts <- readMetaTyVar tv 
 	     ; case cts of
 		 Indirect ty -> loop n args_so_far ty
-		 Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
-			     ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty
-			     ; return (idHsWrapper, res) } }
+		 Flexi -> 
+                   do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
+		      ; res <- thing_inside (reverse args_so_far ++ arg_tys) 
+                                            res_ty
+		      ; return (idHsWrapper, res) } }
+        | otherwise             -- defer as tyvar may be refined by equalities
+        = defer n args_so_far ty
 	where
 	  mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
 	  mk_res_ty [] = panic "TcUnify.mk_res_ty1"
@@ -174,6 +193,21 @@ subFunTys error_herald n_pats res_ty thing_inside
 
     loop n args_so_far res_ty = bale_out args_so_far
 
+         -- build a template type a1 -> ... -> an -> b and defer an equality
+         -- between that template and the expected result type res_ty; then,
+         -- use the template to type the thing_inside
+    defer n args_so_far ty
+      = do { arg_tys <- newFlexiTyVarTys n argTypeKind
+           ; res_ty' <- newFlexiTyVarTy openTypeKind
+           ; let fun_ty = mkFunTys arg_tys res_ty'
+                 err    = error_herald <> comma $$
+                          text "which does not match its type"
+           ; coi <- addErrCtxt err $
+                      defer_unification False False fun_ty ty
+           ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
+           ; return (coiToHsWrapper coi, res)
+           }
+
     bale_out args_so_far 
 	= do { env0 <- tcInitTidyEnv
 	     ; res_ty' <- zonkTcType res_ty
@@ -191,8 +225,9 @@ subFunTys error_herald n_pats res_ty thing_inside
 ----------------------
 boxySplitTyConApp :: TyCon			-- T :: k1 -> ... -> kn -> *
 	          -> BoxyRhoType 		-- Expected type (T a b c)
-		  -> TcM [BoxySigmaType]	-- Element types, a b c
-  -- It's used for wired-in tycons, so we call checkWiredInTyCOn
+		  -> TcM ([BoxySigmaType],	-- Element types, a b c
+                          CoercionI)
+  -- It's used for wired-in tycons, so we call checkWiredInTyCon
   -- Precondition: never called with FunTyCon
   -- Precondition: input type :: *
 
@@ -203,14 +238,28 @@ boxySplitTyConApp tc orig_ty
     loop n_req args_so_far ty 
       | Just ty' <- tcView ty = loop n_req args_so_far ty'
 
-    loop n_req args_so_far (TyConApp tycon args)
+    loop n_req args_so_far ty@(TyConApp tycon args)
       | tc == tycon
       = ASSERT( n_req == length args) 	-- ty::*
-	return (args ++ args_so_far)
+	return (args ++ args_so_far, IdCo)
+
+      | isOpenSynTyCon tycon        -- try to normalise type family application
+      = do { (coi1, ty') <- tcNormaliseFamInst ty
+           ; traceTc $ text "boxySplitTyConApp:" <+> 
+                       ppr ty <+> text "==>" <+> ppr ty'
+           ; case coi1 of
+	       IdCo   -> defer    -- no progress, but maybe solvable => defer
+               ACo _  ->          -- progress: so lets try again
+        	 do { (args, coi2) <- loop n_req args_so_far ty'
+		    ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
+		    }
+           }
 
     loop n_req args_so_far (AppTy fun arg)
       | n_req > 0
-      = loop (n_req - 1) (arg:args_so_far) fun
+      = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun
+           ; return (args, mkAppTyCoI fun coi arg IdCo)
+           }
 
     loop n_req args_so_far (TyVarTy tv)
       | isTyConableTyVar tv
@@ -219,23 +268,42 @@ boxySplitTyConApp tc orig_ty
 	   ; case cts of
 	       Indirect ty -> loop n_req args_so_far ty
 	       Flexi       -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
-				 ; return (arg_tys ++ args_so_far) }
-	}
+				 ; return (arg_tys ++ args_so_far, IdCo) }
+	   }
+      | otherwise             -- defer as tyvar may be refined by equalities
+      = defer
       where
-	mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
 	(arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
 
-    loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
+    loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc)))
+                                  orig_ty
+
+    -- defer splitting by generating an equality constraint
+    defer = boxySplitDefer arg_kinds mk_res_ty orig_ty
+      where
+        (arg_kinds, _) = splitKindFunTys (tyConKind tc)
+
+    -- apply splitted tycon to arguments
+    mk_res_ty = mkTyConApp tc
 
 ----------------------
-boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType	-- Special case for lists
-boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty
-			    ; return elt_ty }
+boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
+-- Special case for lists
+boxySplitListTy exp_ty 
+ = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty
+      ; return (elt_ty, coi) }
 
+----------------------
+boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
+-- Special case for parrs
+boxySplitPArrTy exp_ty 
+  = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty
+       ; return (elt_ty, coi) }
 
 ----------------------
 boxySplitAppTy :: BoxyRhoType				-- Type to split: m a
-	       -> TcM (BoxySigmaType, BoxySigmaType)	-- Returns m, a
+	       -> TcM ((BoxySigmaType, BoxySigmaType),	-- Returns m, a
+                       CoercionI)
 -- If the incoming type is a mutable type variable of kind k, then 
 -- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
 -- If the incoming type is boxy, then so are the result types; and vice versa
@@ -248,18 +316,29 @@ boxySplitAppTy orig_ty
 
     loop ty 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
-      = return (fun_ty, arg_ty)
+      = return ((fun_ty, arg_ty), IdCo)
+
+    loop ty@(TyConApp tycon args)
+      | isOpenSynTyCon tycon        -- try to normalise type family application
+      = do { (coi1, ty') <- tcNormaliseFamInst ty
+           ; case coi1 of
+	       IdCo   -> defer    -- no progress, but maybe solvable => defer
+               ACo co ->          -- progress: so lets try again
+        	 do { (args, coi2) <- loop ty'
+		    ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
+		    }
+           }
 
     loop (TyVarTy tv)
       | isTyConableTyVar tv
       = do { cts <- readMetaTyVar tv
 	   ; case cts of
 	       Indirect ty -> loop ty
-	       Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty
-				 ; return (fun_ty, arg_ty) } }
+	       Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty
+			   ; return ((fun_ty, arg_ty), IdCo) } }
+      | otherwise             -- defer as tyvar may be refined by equalities
+      = defer
       where
-        mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
-	mk_res_ty other = panic "TcUnify.mk_res_ty2"
 	tv_kind = tyVarKind tv
 	kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
 					 	-- m :: * -> k
@@ -271,11 +350,36 @@ boxySplitAppTy orig_ty
 	
     loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
 
+    -- defer splitting by generating an equality constraint
+    defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty
+               ; return ((ty1, ty2), coi)
+               }
+      where
+	orig_kind = typeKind orig_ty
+	arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind),
+					 	-- m :: * -> k
+		     liftedTypeKind]		-- arg type :: *
+ 
+    -- build type application
+    mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
+    mk_res_ty _other             = panic "TcUnify.mk_res_ty2"
+
 ------------------
 boxySplitFailure actual_ty expected_ty
   = unifyMisMatch False False actual_ty expected_ty
 	-- "outer" is False, so we don't pop the context
 	-- which is what we want since we have not pushed one!
+
+------------------
+boxySplitDefer :: [Kind]                   -- kinds of required arguments
+               -> ([TcType] -> TcTauType)  -- construct lhs from argument tyvars
+               -> BoxyRhoType              -- type to split
+               -> TcM ([TcType], CoercionI)
+boxySplitDefer kinds mkTy orig_ty
+  = do { tau_tys <- mapM newFlexiTyVarTy kinds
+       ; coi <- defer_unification False False (mkTy tau_tys) orig_ty
+       ; return (tau_tys, coi)
+       }
 \end{code}
 
 
@@ -649,9 +753,7 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
 	; traceTc (case coi of 
 			IdCo   -> text "tc_sub1 (Rule SBOXY) IdCo"
 			ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
-	; return $ case coi of
-			IdCo   -> idHsWrapper 
-			ACo co -> WpCo co
+	; return $ coiToHsWrapper coi
 	}
 
 -----------------------------------
@@ -763,9 +865,7 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
 defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
   = do	{ coi <- addSubCtxt sub_ctxt act_sty exp_sty $
 	  u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
-	; return $ case coi of
-			IdCo   -> idHsWrapper 
-			ACo co -> WpCo co
+	; return $ coiToHsWrapper coi
 	}
   where
     outer = case sub_ctxt of		-- Ugh
@@ -1318,12 +1418,10 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2)
 uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2
   =     -- ty2 is not a type variable
     case details1 of	
-	MetaTv (SigTv _) _ -> rigid_variable
-	MetaTv info ref1   -> 
-          do { uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2 
-             ; return IdCo
-             }
-	SkolemTv _         -> rigid_variable
+      MetaTv (SigTv _) _ -> rigid_variable
+      MetaTv info ref1   -> 
+        uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2 
+      SkolemTv _         -> rigid_variable
   where
     rigid_variable 
       | isOpenSynTyConApp non_var_ty2
@@ -1399,14 +1497,15 @@ defer_unification outer False ty1 ty2
 	; return $ ACo $ TyVarTy cotv  }
 
 ----------------
-uMetaVar :: SwapFlag
+uMetaVar :: Bool               -- pop innermost context?
+         -> SwapFlag
 	 -> TcTyVar -> BoxInfo -> IORef MetaDetails
 	 -> TcType -> TcType
-	 -> TcM ()
+	 -> TcM CoercionI
 -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
 -- ty2 is not a type variable
 
-uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
+uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
   = 	-- tv1 is a BoxTv.  So we must unbox ty2, to ensure
 	-- that any boxes in ty2 are filled with monotypes
 	-- 
@@ -1422,11 +1521,21 @@ uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
 			   return ()	-- This really should *not* happen
 	    Flexi -> return ()
 #endif
-	; checkUpdateMeta swapped tv1 ref1 final_ty }
+	; checkUpdateMeta swapped tv1 ref1 final_ty
+        ; return IdCo
+        }
 
-uMetaVar swapped tv1 info1 ref1 ps_ty2 non_var_ty2
-  = do	{ final_ty <- checkTauTvUpdate tv1 ps_ty2	-- Occurs check + monotype check
-	; checkUpdateMeta swapped tv1 ref1 final_ty }
+uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2
+  = do	{ -- Occurs check + monotype check
+        ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2
+        ; case mb_final_ty of
+            Nothing       ->    -- tv1 occured in type family parameter
+              defer_unification outer swapped (mkTyVarTy tv1) ps_ty2
+            Just final_ty -> 
+              do { checkUpdateMeta swapped tv1 ref1 final_ty 
+                 ; return IdCo
+                 }
+        }
 
 ----------------
 uUnfilledVars :: Outer
@@ -1505,26 +1614,6 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
 	-- a user-written type sig
 \end{code}
 
-Note [Type synonyms and the occur check]
-~~~~~~~~~~~~~~~~~~~~
-Basically we want to update     tv1 := ps_ty2
-because ps_ty2 has type-synonym info, which improves later error messages
-
-But consider 
-	type A a = ()
-
-	f :: (A a -> a -> ()) -> ()
-	f = \ _ -> ()
-
-	x :: ()
-	x = f (\ x p -> p x)
-
-In the application (p x), we try to match "t" with "A t".  If we go
-ahead and bind t to A t (= ps_ty2), we'll lead the type checker into 
-an infinite loop later.
-But we should not reject the program, because A t = ().
-Rather, we should bind t to () (= non_var_ty2).
-
 \begin{code}
 refineBox :: TcType -> TcM TcType
 -- Unbox the outer box of a boxy type (if any)
@@ -1664,13 +1753,9 @@ unifyForAllCtxt tvs phi1 phi2 env
 
 -----------------------
 unifyMisMatch outer swapped ty1 ty2
-  = do	{ (env, msg) <- if swapped then misMatchMsg ty2 ty1
-				   else misMatchMsg ty1 ty2
-
-	-- This is the whole point of the 'outer' stuff
-	; if outer then popErrCtxt (failWithTcM (env, msg))
-	  	   else failWithTcM (env, msg)
-	} 
+  | swapped   = unifyMisMatch outer False ty2 ty1
+  | outer     = popErrCtxt $ unifyMisMatch False swapped ty1 ty2  -- This is the whole point of the 'outer' stuff
+  | otherwise = failWithMisMatch ty1 ty2
 \end{code}