Improve occurs-check error reporting (fix Trac #6123)

We were wrongly reporting (a ~ F a) as an occurs-check error
when F is a type function.

3 files changed, 80 insertions, 78 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 2e87c9e2f2..8a45632bfb 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -7,7 +7,7 @@
 -- for details
 
 module TcCanonical(
-    canonicalize, flatten, flattenMany, 
+    canonicalize, flatten, flattenMany, occurCheckExpand,
     FlattenMode (..),
     StopOrContinue (..)
  ) where
@@ -1290,8 +1290,8 @@ canEqLeafTyVarLeft d fl tv s2       -- eqv : tv ~ s2
            return Stop
          else do
        -- Not reflexivity but maybe an occurs error
-       { occ_check_result <- canOccursCheck fl tv xi2
-       ; let xi2' = fromMaybe xi2 occ_check_result
+       { let occ_check_result = occurCheckExpand tv xi2
+             xi2' = fromMaybe xi2 occ_check_result
              
              not_occ_err = isJust occ_check_result
                   -- Delicate: don't want to cache as solved a constraint with occurs error!
@@ -1307,28 +1307,20 @@ canEqLeafTyVarLeft d fl tv s2       -- eqv : tv ~ s2
                             canEqFailure d new_fl
            Nothing -> return Stop
         } }
-
--- See Note [Type synonyms and canonicalization].
--- Check whether the given variable occurs in the given type.  We may
--- have needed to do some type synonym unfolding in order to get rid
--- of the variable, so we also return the unfolded version of the
--- type, which is guaranteed to be syntactically free of the given
--- type variable.  If the type is already syntactically free of the
--- variable, then the same type is returned.
---
--- Precondition: the two types are not equal (looking though synonyms)
-canOccursCheck :: CtEvidence -> TcTyVar -> Xi -> TcS (Maybe Xi)
-canOccursCheck _gw tv xi = return (expandAway tv xi)
 \end{code}
 
-@expandAway tv xi@ expands synonyms in xi just enough to get rid of
-occurrences of tv, if that is possible; otherwise, it returns Nothing.
+Note [Occurs check expansion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+@occurCheckExpand tv xi@ expands synonyms in xi just enough to get rid
+of occurrences of tv outside type function arguments, if that is
+possible; otherwise, it returns Nothing.
+
 For example, suppose we have
   type F a b = [a]
 Then
-  expandAway b (F Int b) = Just [Int]
+  occurCheckExpand b (F Int b) = Just [Int]
 but
-  expandAway a (F a Int) = Nothing
+  occurCheckExpand a (F a Int) = Nothing
 
 We don't promise to do the absolute minimum amount of expanding
 necessary, but we try not to do expansions we don't need to.  We
@@ -1336,49 +1328,61 @@ prefer doing inner expansions first.  For example,
   type F a b = (a, Int, a, [a])
   type G b   = Char
 We have
-  expandAway b (F (G b)) = F Char
+  occurCheckExpand b (F (G b)) = F Char
 even though we could also expand F to get rid of b.
 
+See also Note [Type synonyms and canonicalization].
+
 \begin{code}
-expandAway :: TcTyVar -> Xi -> Maybe Xi
-expandAway tv t@(TyVarTy tv')
-  | tv == tv' = Nothing
-  | otherwise = Just t
-expandAway tv xi
-  | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
-expandAway tv (AppTy ty1 ty2) 
-  = do { ty1' <- expandAway tv ty1
-       ; ty2' <- expandAway tv ty2 
-       ; return (mkAppTy ty1' ty2') }
--- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
-expandAway tv (FunTy ty1 ty2)
-  = do { ty1' <- expandAway tv ty1 
-       ; ty2' <- expandAway tv ty2 
-       ; return (mkFunTy ty1' ty2') } 
--- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
-expandAway tv ty@(ForAllTy {}) 
-  = let (tvs,rho) = splitForAllTys ty
-        tvs_knds  = map tyVarKind tvs 
-    in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
-       -- Can't expand away the kinds unless we create 
-       -- fresh variables which we don't want to do at this point.
-           Nothing 
-       else do { rho' <- expandAway tv rho
-               ; return (mkForAllTys tvs rho') }
--- For a type constructor application, first try expanding away the
--- offending variable from the arguments.  If that doesn't work, next
--- see if the type constructor is a type synonym, and if so, expand
--- it and try again.
-expandAway tv ty@(TyConApp tc tys)
-  = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
-
-expandAway _ xi@(LitTy {}) = return xi
+occurCheckExpand :: TcTyVar -> Type -> Maybe Type
+-- Check whether the given variable occurs in the given type.  We may
+-- have needed to do some type synonym unfolding in order to get rid
+-- of the variable, so we also return the unfolded version of the
+-- type, which is guaranteed to be syntactically free of the given
+-- type variable.  If the type is already syntactically free of the
+-- variable, then the same type is returned.
 
+occurCheckExpand tv ty
+  | not (tv `elemVarSet` tyVarsOfType ty) = Just ty
+  | otherwise                             = go ty
+  where
+    go t@(TyVarTy tv') | tv == tv' = Nothing
+                       | otherwise = Just t
+    go ty@(LitTy {}) = return ty
+    go (AppTy ty1 ty2) = do { ty1' <- go ty1
+           		    ; ty2' <- go ty2  
+           		    ; return (mkAppTy ty1' ty2') }
+    -- mkAppTy <$> go ty1 <*> go ty2
+    go (FunTy ty1 ty2) = do { ty1' <- go ty1 
+           		    ; ty2' <- go ty2 
+           		    ; return (mkFunTy ty1' ty2') } 
+    -- mkFunTy <$> go ty1 <*> go ty2
+    go ty@(ForAllTy {})
+       | tv `elemVarSet` tyVarsOfTypes tvs_knds = Nothing
+           -- Can't expand away the kinds unless we create 
+           -- fresh variables which we don't want to do at this point.
+       | otherwise = do { rho' <- go rho
+                        ; return (mkForAllTys tvs rho') }
+       where
+         (tvs,rho) = splitForAllTys ty
+         tvs_knds  = map tyVarKind tvs 
+
+    -- For a type constructor application, first try expanding away the
+    -- offending variable from the arguments.  If that doesn't work, next
+    -- see if the type constructor is a type synonym, and if so, expand
+    -- it and try again.
+    go ty@(TyConApp tc tys)
+      | isSynFamilyTyCon tc    -- It's ok for tv to occur under a type family application
+       = return ty             -- Eg.  (a ~ F a) is not an occur-check error
+                               -- NB This case can't occur during canonicalisation,
+                               --    because the arg is a Xi-type, but can occur in the
+                               --    call from TcErrors
+      | otherwise
+      = (mkTyConApp tc <$> mapM go tys) <|> (tcView ty >>= go)
 \end{code}
 
 Note [Type synonyms and canonicalization]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 We treat type synonym applications as xi types, that is, they do not
 count as type function applications.  However, we do need to be a bit
 careful with type synonyms: like type functions they may not be
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 483de071d4..781918ddf9 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -17,6 +17,7 @@ module TcErrors(
 
 #include "HsVersions.h"
 
+import TcCanonical( occurCheckExpand )
 import TcRnMonad
 import TcMType
 import TcType
@@ -455,17 +456,20 @@ mkEqErr1 ctxt ct
         msg   = mkExpectedActualMsg exp act
     mk_err ctxt1 _ = mkEqErr_help ctxt1 ct False ty1 ty2
 
-mkEqErr_help :: ReportErrCtxt
-             -> Ct
-             -> Bool     -- True  <=> Types are correct way round;
-                         --           report "expected ty1, actual ty2"
-                         -- False <=> Just report a mismatch without orientation
-                         --           The ReportErrCtxt has expected/actual 
-             -> TcType -> TcType -> TcM ErrMsg
+mkEqErr_help, reportEqErr 
+   :: ReportErrCtxt
+   -> Ct
+   -> Bool     -- True  <=> Types are correct way round;
+               --           report "expected ty1, actual ty2"
+               -- False <=> Just report a mismatch without orientation
+               --           The ReportErrCtxt has expected/actual 
+   -> TcType -> TcType -> TcM ErrMsg
 mkEqErr_help ctxt ct oriented ty1 ty2
   | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt ct oriented tv1 ty2
   | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt ct oriented tv2 ty1
-  | otherwise   -- Neither side is a type variable
+  | otherwise                        = reportEqErr ctxt ct oriented ty1 ty2
+
+reportEqErr ctxt ct oriented ty1 ty2
   = do { ctxt' <- mkEqInfoMsg ctxt ct ty1 ty2
        ; mkErrorReport ctxt' (misMatchOrCND ctxt' ct oriented ty1 ty2) }
 
@@ -484,7 +488,7 @@ mkTyVarEqErr ctxt ct oriented tv1 ty2
   = mkErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2)
 
   -- Occurs check
-  | tv1 `elemVarSet` tyVarsOfType ty2
+  | isNothing (occurCheckExpand tv1 ty2)
   = let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
                            (sep [ppr ty1, char '=', ppr ty2])
     in mkErrorReport ctxt occCheckMsg
@@ -524,21 +528,10 @@ mkTyVarEqErr ctxt ct oriented tv1 ty2
        ; mkErrorReport (addExtraTyVarInfo ctxt ty1 ty2) (msg $$ nest 2 extra) }
 
   | otherwise
-  = pprTrace "mkTyVarEqErr" (ppr tv1 $$ ppr ty2 $$ ppr (cec_encl ctxt)) $
-    panic "mkTyVarEqErr"
-    	-- I don't think this should happen, and if it does I want to know
-	-- Trac #5130 happened because an actual type error was not
-	-- reported at all!  So not reporting is pretty dangerous.
-	-- 
-	-- OLD, OUT OF DATE COMMENT
-        -- This can happen, by a recursive decomposition of frozen
-        -- occurs check constraints
-        -- Example: alpha ~ T Int alpha has frozen.
-        --          Then alpha gets unified to T beta gamma
-        -- So now we have  T beta gamma ~ T Int (T beta gamma)
-        -- Decompose to (beta ~ Int, gamma ~ T beta gamma)
-        -- The (gamma ~ T beta gamma) is the occurs check, but
-        -- the (beta ~ Int) isn't an error at all.  So return ()
+  = reportEqErr ctxt ct oriented (mkTyVarTy tv1) ty2
+        -- This *can* happen (Trac #6123, and test T2627b)
+        -- Consider an ambiguous top-level constraint (a ~ F a)
+        -- Not an occurs check, becuase F is a type function.
   where         
     k1 	= tyVarKind tv1
     k2 	= typeKind ty2
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index e3b6a33298..2a735fe77f 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -593,6 +593,11 @@ solveWithIdentity :: SubGoalDepth
 --     must work for Derived as well as Wanted
 -- Returns: workItem where 
 --        workItem = the new Given constraint
+--
+-- NB: No need for an occurs check here, because solveWithIdentity always 
+--     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
+--     say that in (a ~ xi), the type variable a does not appear in xi.
+--     See TcRnTypes.Ct invariants.
 solveWithIdentity d wd tv xi 
   = do { let tv_ty = mkTyVarTy tv
        ; traceTcS "Sneaky unification:" $