From 6493f9d3305d5af08ad92c8f32b8b6410404eb46 Mon Sep 17 00:00:00 2001
From: "simonpj@microsoft.com" <unknown>
Date: Tue, 1 Aug 2006 21:43:02 +0000
Subject: [PATCH] Make unification robust to a boxy type variable meeting
 itself

Previously, the implicit assumption in unification is that a boxy
type variable could never occur on both sides of the unification,
so that we'd never find
	bx5 :=: bx5

But the pre-subsumption stuff really means that the same variable
can occur on both sides.  Consider
	forall a. a->Int <= bx5->Int
Then pre-subumption will find a->bx5; and the full subsumption step
will find bx5:=bx5.

However, I think there is still no possiblity of a full occurs-check
failure; that is,
	bx5 :=: Tree bx5
Although I can't quite see how to prove it!  So I've added a
DEBUG test in uMetaVar to check for this case.
---
 compiler/typecheck/TcUnify.lhs |   38 +++++++++++++++++++++++++++++---------
 1 file changed, 29 insertions(+), 9 deletions(-)

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index e00c8ef..1a61822 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -478,8 +478,8 @@ boxyLub orig_ty1 orig_ty2
       = TyConApp tc1 (zipWith boxyLub ts1 ts2)
 
     go (TyVarTy tv1) ty2		-- This is the whole point; 
-      | isTcTyVar tv1, isMetaTyVar tv1 	-- choose ty2 if ty2 is a box
-      = ty2	
+      | isTcTyVar tv1, isBoxyTyVar tv1 	-- choose ty2 if ty2 is a box
+      = orig_ty2	
 
 	-- Look inside type synonyms, but only if the naive version fails
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
@@ -996,10 +996,14 @@ uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2
   = 	-- Expand synonyms; ignore FTVs
     uUnfilledVar False swapped tv1 details1 nb2 ps_ty2 ty2'
 
-uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2@(TyVarTy tv2)
-	-- Same type variable => no-op
-  | tv1 == tv2
-  = returnM ()
+uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 (TyVarTy tv2)
+  | tv1 == tv2	-- Same type variable => no-op (but watch out for the boxy case)
+  = case details1 of
+	MetaTv BoxTv ref1  -- A boxy type variable meets itself;
+			   -- this is box-meets-box, so fill in with a tau-type
+	      -> do { tau_tv <- tcInstTyVar tv1
+		    ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) }
+	other -> returnM ()	-- No-op
 
 	-- Distinct type variables
   | otherwise
@@ -1025,10 +1029,26 @@ uMetaVar :: Bool
 -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
 -- ty2 is not a type variable
 
+uMetaVar swapped tv1 BoxTv ref1 nb2 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
+	-- 
+	-- It should not be the case that tv1 occurs in ty2
+	-- (i.e. no occurs check should be needed), but if perchance
+	-- it does, the unbox operation will fill it, and the DEBUG
+	-- checks for that.
+    do 	{ final_ty <- unBox ps_ty2
+#ifdef DEBUG
+	; meta_details <- readMutVar ref1
+	; case meta_details of
+	    Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
+			   return ()	-- This really should *not* happen
+	    Flexi       -> return ()
+#endif
+	; checkUpdateMeta swapped tv1 ref1 final_ty }
+
 uMetaVar swapped tv1 info1 ref1 nb2 ps_ty2 non_var_ty2
-  = do	{ final_ty <- case info1 of
-			BoxTv -> unBox ps_ty2			-- No occurs check
-			other -> checkTauTvUpdate tv1 ps_ty2	-- Occurs check + monotype check
+  = do	{ final_ty <- checkTauTvUpdate tv1 ps_ty2	-- Occurs check + monotype check
 	; checkUpdateMeta swapped tv1 ref1 final_ty }
 
 ----------------
-- 
1.7.10.4