Update Trac ticket URLs to point to GitLab
[ghc.git] / compiler / types / Type.hs
index 473e9e5..4426148 100644 (file)
@@ -14,7 +14,7 @@ module Type (
         -- $type_classification
 
         -- $representation_types
-        TyThing(..), Type, ArgFlag(..), AnonArgFlag,
+        TyThing(..), Type, ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
         KindOrType, PredType, ThetaType,
         Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder,
         KnotTied,
@@ -42,7 +42,7 @@ module Type (
         mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInvForAllTy, mkInvForAllTys,
-        splitForAllTys, splitForAllVarBndrs,
+        splitForAllTys, splitForAllTysSameVis, splitForAllVarBndrs,
         splitForAllTy_maybe, splitForAllTy,
         splitForAllTy_ty_maybe, splitForAllTy_co_maybe,
         splitPiTy_maybe, splitPiTy, splitPiTys,
@@ -349,7 +349,7 @@ We implement this by making 'coreView' convert 'Constraint' to 'TYPE
 LiftedRep' on the fly.  The function tcView (used in the type checker)
 does not do this.
 
-See also Trac #11715, which tracks removing this inconsistency.
+See also #11715, which tracks removing this inconsistency.
 
 -}
 
@@ -415,7 +415,7 @@ expandTypeSynonyms ty
             --     /idempotent/ substitution, even in the nested case
             --        type T a b = a -> b
             --        type S x y = T y x
-            -- (Trac #11665)
+            -- (#11665)
         in  mkAppTys (go subst' rhs) tys'
       | otherwise
       = TyConApp tc expanded_tys
@@ -686,7 +686,7 @@ Note [Decomposing fat arrow c=>t]
 Can we unify (a b) with (Eq a => ty)?   If we do so, we end up with
 a partial application like ((=>) Eq a) which doesn't make sense in
 source Haskell.  In contrast, we *can* unify (a b) with (t1 -> t2).
-Here's an example (Trac #9858) of how you might do it:
+Here's an example (#9858) of how you might do it:
    i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
    i p = typeRep p
 
@@ -1066,7 +1066,7 @@ piResultTys ty orig_args@(arg:args)
         -- have the right kind to apply to them; so panic.
         -- Without the explicit isEmptyVarEnv test, an ill-kinded type
         -- would give an infniite loop, which is very unhelpful
-        -- c.f. Trac #15473
+        -- c.f. #15473
         pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
 
 applyTysX :: [TyVar] -> Type -> [Type] -> Type
@@ -1098,7 +1098,7 @@ So
 
 In other words we must intantiate the forall!
 
-Similarly (Trac #15428)
+Similarly (#15428)
    S :: forall k f. k -> f k
 and we are finding the kind of
    S * (* ->) Int Bool
@@ -1400,7 +1400,7 @@ with a fat arrow; that is, using mkInvisFunTy, not mkVisFunTy.
 
 Why? After all, we are in Core, where (=>) and (->) behave the same.
 Yes, but the /specialiser/ does treat dictionary arguments specially.
-Suppose we do w/w on 'foo' in module A, thus (Trac #11272, #6056)
+Suppose we do w/w on 'foo' in module A, thus (#11272, #6056)
    foo :: Ord a => Int -> blah
    foo a d x = case x of I# x' -> $wfoo @a d x'
 
@@ -1455,6 +1455,18 @@ splitForAllTys ty = split ty ty []
     split _       (ForAllTy (Bndr tv _) ty)    tvs = split ty ty (tv:tvs)
     split orig_ty _                            tvs = (reverse tvs, orig_ty)
 
+-- | Like 'splitForAllTys', but only splits a 'ForAllTy' if
+-- @'sameVis' argf supplied_argf@ is 'True', where @argf@ is the visibility
+-- of the @ForAllTy@'s binder and @supplied_argf@ is the visibility provided
+-- as an argument to this function.
+splitForAllTysSameVis :: ArgFlag -> Type -> ([TyCoVar], Type)
+splitForAllTysSameVis supplied_argf ty = split ty ty []
+  where
+    split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
+    split _       (ForAllTy (Bndr tv argf) ty) tvs
+      | argf `sameVis` supplied_argf               = split ty ty (tv:tvs)
+    split orig_ty _                            tvs = (reverse tvs, orig_ty)
+
 -- | Like splitForAllTys, but split only for tyvars.
 -- This always succeeds, even if it returns only an empty list. Note that the
 -- result type returned may have free variables that were bound by a forall.
@@ -1667,7 +1679,7 @@ tyConArgFlags tc = fun_kind_arg_flags (tyConKind tc)
 -- 'Specified' and the second argument (@Bool@) is 'Required'. It is precisely
 -- this sort of higher-rank situation in which 'appTyArgFlags' comes in handy,
 -- since @f Type Bool@ would be represented in Core using 'AppTy's.
--- (See also Trac #15792).
+-- (See also #15792).
 appTyArgFlags :: Type -> [Type] -> [ArgFlag]
 appTyArgFlags ty = fun_kind_arg_flags (typeKind ty)
 
@@ -2417,7 +2429,7 @@ and now we can make f' a join point:
   in ... jump f' 1 'b' ... jump f' 2 'c' ...
 
 It's not clear that this comes up often, however. TODO: Measure how often and
-add this analysis if necessary.  See Trac #14620.
+add this analysis if necessary.  See #14620.
 
 
 ************************************************************************
@@ -2700,6 +2712,30 @@ In tcTypeKind we consider Constraint and (TYPE LiftedRep) to be distinct:
 Note that:
 * The only way we distinguish '->' from '=>' is by the fact
   that the argument is a PredTy.  Both are FunTys
+
+Note [Phantom type variables in kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  type K (r :: RuntimeRep) = Type   -- Note 'r' is unused
+  data T r :: K r                   -- T :: forall r -> K r
+  foo :: forall r. T r
+
+The body of the forall in foo's type has kind (K r), and
+normally it would make no sense to have
+   forall r. (ty :: K r)
+because the kind of the forall would escape the binding
+of 'r'.  But in this case it's fine because (K r) exapands
+to Type, so we expliclity /permit/ the type
+   forall r. T r
+
+To accommodate such a type, in typeKind (forall a.ty) we use
+occCheckExpand to expand any type synonyms in the kind of 'ty'
+to eliminate 'a'.  See kinding rule (FORALL) in
+Note [Kinding rules for types]
+
+And in TcValidity.checkEscapingKind, we use also use
+occCheckExpand, for the same reason.
 -}
 
 -----------------------------
@@ -2722,8 +2758,11 @@ typeKind (AppTy fun arg)
     go fun             args = piResultTys (typeKind fun) args
 
 typeKind ty@(ForAllTy {})
-  = case occCheckExpand tvs body_kind of   -- We must make sure tv does not occur in kind
-      Just k' -> k'                        -- As it is already out of scope!
+  = case occCheckExpand tvs body_kind of
+      -- We must make sure tv does not occur in kind
+      -- As it is already out of scope!
+      -- See Note [Phantom type variables in kinds]
+      Just k' -> k'
       Nothing -> pprPanic "typeKind"
                   (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
   where
@@ -2760,8 +2799,11 @@ tcTypeKind ty@(ForAllTy {})
   = constraintKind
 
   | otherwise
-  = case occCheckExpand tvs body_kind of   -- We must make sure tv does not occur in kind
-      Just k' -> k'                        -- As it is already out of scope!
+  = case occCheckExpand tvs body_kind of
+      -- We must make sure tv does not occur in kind
+      -- As it is already out of scope!
+      -- See Note [Phantom type variables in kinds]
+      Just k' -> k'
       Nothing -> pprPanic "tcTypeKind"
                   (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
   where