Fix Trac #3409: type synonyms that discard their arguments

Type synonyms that don't mention one of their type parameters on the
RHS are a pain in the neck.  This patch fixes a long-standing bug (that
simply has not appeared before) in that exprType could return a type
mentioning an existentially-quantified variable (in one of those ignored
argument positions).

See CoreUtils Note [Existential variables and silly type synonyms]

The fix is not entirely beautiful, but it works, and is very localised.

diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs
index 95f35af..869f356 100644 (file)
--- a/compiler/coreSyn/CoreUtils.lhs
+++ b/compiler/coreSyn/CoreUtils.lhs
@@ -51,6 +51,7 @@ import PprCore
 import Var
 import SrcLoc
 import VarEnv
+import VarSet
 import Name
 import Module
 #if mingw32_TARGET_OS
@@ -103,7 +104,13 @@ exprType other = pprTrace "exprType" (pprCoreExpr other) alphaTy
 
 coreAltType :: CoreAlt -> Type
 -- ^ Returns the type of the alternatives right hand side
-coreAltType (_,_,rhs) = exprType rhs
+coreAltType (_,bs,rhs) 
+  | any bad_binder bs = expandTypeSynonyms ty
+  | otherwise         = ty    -- Note [Existential variables and silly type synonyms]
+  where
+    ty           = exprType rhs
+    free_tvs     = tyVarsOfType ty
+    bad_binder b = isTyVar b && b `elemVarSet` free_tvs
 
 coreAltsType :: [CoreAlt] -> Type
 -- ^ Returns the type of the first alternative, which should be the same as for all alternatives
@@ -111,6 +118,30 @@ coreAltsType (alt:_) = coreAltType alt
 coreAltsType []             = panic "corAltsType"
 \end{code}
 
+Note [Existential variables and silly type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+       data T = forall a. T (Funny a)
+       type Funny a = Bool
+       f :: T -> Bool
+       f (T x) = x
+
+Now, the type of 'x' is (Funny a), where 'a' is existentially quantified.
+That means that 'exprType' and 'coreAltsType' may give a result that *appears*
+to mention an out-of-scope type variable.  See Trac #3409 for a more real-world
+example.
+
+Various possibilities suggest themselves:
+
+ - Ignore the problem, and make Lint not complain about such variables
+
+ - Expand all type synonyms (or at least all those that discard arguments)
+      This is tricky, because at least for top-level things we want to
+      retain the type the user originally specified.
+
+ - Expand synonyms on the fly, when the problem arises. That is what
+   we are doing here.  It's not too expensive, I think.
+
 \begin{code}
 mkPiType  :: Var   -> Type -> Type
 -- ^ Makes a @(->)@ type or a forall type, depending

diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 3705914..d34a64c 100644 (file)
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -87,7 +87,7 @@ module Type (
 
        -- * Type free variables
        tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-       typeKind,
+       typeKind, expandTypeSynonyms,
 
        -- * Tidying type related things up for printing
        tidyType,      tidyTypes,
@@ -281,6 +281,29 @@ tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
 tcView _                 = Nothing
 
 -----------------------------------------------
+expandTypeSynonyms :: Type -> Type
+-- ^ Expand out all type synonyms.  Actually, it'd suffice to expand out
+-- just the ones that discard type variables (e.g.  type Funny a = Int)
+-- But we don't know which those are currently, so we just expand all.
+expandTypeSynonyms ty 
+  = go ty
+  where
+    go (TyConApp tc tys)
+      | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys 
+      = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
+      | otherwise
+      = TyConApp tc (map go tys)
+    go (TyVarTy tv)    = TyVarTy tv
+    go (AppTy t1 t2)   = AppTy (go t1) (go t2)
+    go (FunTy t1 t2)   = FunTy (go t1) (go t2)
+    go (ForAllTy tv t) = ForAllTy tv (go t)
+    go (PredTy p)      = PredTy (go_pred p)
+
+    go_pred (ClassP c ts)  = ClassP c (map go ts)
+    go_pred (IParam ip t)  = IParam ip (go t)
+    go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
+
+-----------------------------------------------
 {-# INLINE kindView #-}
 kindView :: Kind -> Maybe Kind
 -- ^ Similar to 'coreView' or 'tcView', but works on 'Kind's