[commit: ghc] master: Some refactoring of the occurs check in TcUnify (242fc56)

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/242fc5606d5a94205949f8bd58bea348c247d863

>---------------------------------------------------------------

commit 242fc5606d5a94205949f8bd58bea348c247d863
Author: Simon Peyton Jones <[email protected]>
Date:   Fri Oct 19 01:22:20 2012 +0100

    Some refactoring of the occurs check in TcUnify
    
    I was experimenting with allowing unification with a type variable
    when there are type functions in the type; but that led to strangely
    worse error messages (See Note [Conservative unification check]) in
    TcUnify.  I don't quite understand why, but the simple thing for now
    is to maintain the same behaviour.  I tidied up the code a bit though.

>---------------------------------------------------------------

 compiler/typecheck/TcUnify.lhs |  107 ++++++++++++++++++++++------------------
 1 files changed, 59 insertions(+), 48 deletions(-)

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 18c77d7..3a13b9c 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -766,22 +766,19 @@ uUnfilledVar origin swapped tv1 details1 non_var_ty2  -- ty2 is not a type varia
       MetaTv { mtv_info = TauTv, mtv_ref = ref1 }
         -> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2
               ; case mb_ty2' of
-                  Nothing   -> do { traceTc "Occ/kind defer" (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
-                                                              $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
-                                  ; defer }
                   Just ty2' -> updateMeta tv1 ref1 ty2'
+                  Nothing   -> do { traceTc "Occ/kind defer" 
+                                        (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
+                                         $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
+                                  ; defer }
               }
 
       _other -> do { traceTc "Skolem defer" (ppr tv1); defer }	-- Skolems of all sorts
   where
-    defer | Just ty2' <- tcView non_var_ty2	-- Note [Avoid deferring]
-    	    	         	   		-- non_var_ty2 isn't expanded yet
-          = uUnfilledVar origin swapped tv1 details1 ty2'
-          | otherwise
-          = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
-          -- Occurs check or an untouchable: just defer
-	  -- NB: occurs check isn't necessarily fatal: 
-	  --     eg tv1 occured in type family parameter
+    defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
+               -- Occurs check or an untouchable: just defer
+	       -- NB: occurs check isn't necessarily fatal: 
+	       --     eg tv1 occured in type family parameter
 
 ----------------
 uUnfilledVars :: CtOrigin
@@ -855,51 +852,65 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 -- sort matters out.
 
 checkTauTvUpdate tv ty
-  = do { ty'   <- zonkTcType ty
-       ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty')
+  = do { ty1   <- zonkTcType ty
+       ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty1)
        ; case sub_k of
-           Nothing -> return Nothing
-           Just LT -> return Nothing
-           _       -> return (occurCheckExpand tv ty') }
-
-{-
+           Nothing           -> return Nothing
+           Just LT           -> return Nothing
+           _  | defer_me ty1   -- Quick test
+              -> -- Failed quick test so try harder
+                 case occurCheckExpand tv ty1 of 
+                   Nothing -> return Nothing
+                   Just ty2 | defer_me ty2 -> return Nothing
+                            | otherwise    -> return (Just ty2)
+              | otherwise   -> return (Just ty1) }
   where 
-    ok :: TcType -> Maybe TcType 
-    -- This version of TcType.occurCheckExpand checked that ty does 
-    -- not contain any type families, but that's no longer necessary:
-    -- See Note [Type family sharing]
-    -- 
-    -- Checks that tv does not occur in the arg type
-    -- expanding type synonyms where necessary to make this so
-    -- eg type Phantom a = Bool
-    --     ok (tv -> Int)         = Nothing
-    --     ok (x -> Int)          = Just (x -> Int)
-    --     ok (Phantom tv -> Int) = Just (Bool -> Int)
-    ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv') 
-    ok this_ty@(TyConApp tc tys) 
-      | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys) 
-      = Just (TyConApp tc tys') 
-      | isSynTyCon tc, Just ty_expanded <- tcView this_ty
-      = ok ty_expanded -- See Note [Type synonyms and the occur check] 
-    ok ty@(LitTy {}) = Just ty
-    ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res
-                       = Just (FunTy arg' res') 
-    ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg 
-                       = Just (AppTy fun' arg') 
-    ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1') 
-    -- Fall-through 
-    ok _ty = Nothing 
--}
+    defer_me :: TcType -> Bool
+    -- Checks for (a) occurrence of tv
+    --            (b) type family applicatios
+    -- See Note [Conservative unification check]
+    defer_me (LitTy {})        = False
+    defer_me (TyVarTy tv')     = tv == tv'
+    defer_me (TyConApp tc tys) = isSynFamilyTyCon tc || any defer_me tys
+    defer_me (FunTy arg res)   = defer_me arg || defer_me res
+    defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
+    defer_me (ForAllTy _ ty)   = defer_me ty
 \end{code}
 
-Note [Avoid deferring]
-~~~~~~~~~~~~~~~~~~~~~~
-We try to avoid creating deferred constraints only for efficiency.
-Example (Trac #4917)
+Note [Conservative unification check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When unifying (tv ~ rhs), w try to avoid creating deferred constraints
+only for efficiency.  However, we do not unify (the defer_me check) if
+  a) There's an occurs check (tv is in fvs(rhs))
+  b) There's a type-function call in 'rhs'
+
+If we fail defer_me we use occurCheckExpand to try to make it pass,
+(see Note [Type synonyms and the occur check]) and then use defer_me
+again to check.  Example: Trac #4917)
        a ~ Const a b
 where type Const a b = a.  We can solve this immediately, even when
 'a' is a skolem, just by expanding the synonym.
 
+We always defer type-function calls, even if it's be perfectly safe to
+unify, eg (a ~ F [b]).  Reason: this ensures that the constraint
+solver gets to see, and hence simplify the type-function call, which
+in turn might simplify the type of an inferred function.  Test ghci046
+is a case in point.
+
+More mysteriously, test T7010 gave a horrible error 
+  T7010.hs:29:21:
+    Couldn't match type `Serial (ValueTuple Float)' with `IO Float'
+    Expected type: (ValueTuple Vector, ValueTuple Vector)
+      Actual type: (ValueTuple Vector, ValueTuple Vector)
+because an insoluble type function constraint got mixed up with
+a soluble one when flattening.  I never fully understood this, but
+deferring type-function applications made it go away :-(.
+T5853 also got a less-good error message with more aggressive
+unification of type functions.
+
+Moreover the Note [Type family sharing] gives another reason, but
+again I'm not sure if it's really valid.
+
 Note [Type synonyms and the occur check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Generally speaking we try to update a variable with type synonyms not