Refactor the treatment of predicate types
[ghc.git] / compiler / types / Type.hs
index bda3602..3463920 100644 (file)
@@ -62,8 +62,9 @@ module Type (
         coAxNthLHS,
         stripCoercionTy, splitCoercionType_maybe,
 
-        splitPiTysInvisible, filterOutInvisibleTypes,
+        splitPiTysInvisible, filterOutInvisibleTypes, filterOutInferredTypes,
         partitionInvisibleTypes, partitionInvisibles,
+        tyConArgFlags, appTyArgFlags,
         synTyConResKind,
 
         modifyJoinResTy, setJoinResTy,
@@ -109,9 +110,10 @@ module Type (
 
         -- ** Predicates on types
         isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
-        isCoercionTy_maybe, isCoercionType, isForAllTy,
+        isCoercionTy_maybe, isForAllTy,
         isForAllTy_ty, isForAllTy_co,
         isPiTy, isTauTy, isFamFreeTy,
+        isCoVarType, isEvVarType,
 
         isValidJoinPointType,
 
@@ -262,7 +264,6 @@ import Unique ( nonDetCmpUnique )
 import Maybes           ( orElse )
 import Data.Maybe       ( isJust, mapMaybe )
 import Control.Monad    ( guard )
-import Control.Arrow    ( first, second )
 
 -- $type_classification
 -- #type_classification#
@@ -1544,23 +1545,44 @@ splitPiTysInvisible ty = split ty ty []
       | isPredTy arg                   = split res res (Anon arg : bs)
     split orig_ty _                bs  = (reverse bs, orig_ty)
 
--- | Given a tycon and its arguments, filters out any invisible arguments
+-- | Given a 'TyCon' and a list of argument types, filter out any invisible
+-- (i.e., 'Inferred' or 'Specified') arguments.
 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
 filterOutInvisibleTypes tc tys = snd $ partitionInvisibleTypes tc tys
 
--- | Given a 'TyCon' and its arguments, partition the arguments into
--- (invisible arguments, visible arguments).
+-- | Given a 'TyCon' and a list of argument types, filter out any 'Inferred'
+-- arguments.
+filterOutInferredTypes :: TyCon -> [Type] -> [Type]
+filterOutInferredTypes tc tys =
+  filterByList (map (/= Inferred) $ tyConArgFlags tc tys) tys
+
+-- | Given a 'TyCon' and a list of argument types, partition the arguments
+-- into:
+--
+-- 1. 'Inferred' or 'Specified' (i.e., invisible) arguments and
+--
+-- 2. 'Required' (i.e., visible) arguments
 partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
-partitionInvisibleTypes tc tys = partitionInvisibles tc id tys
+partitionInvisibleTypes tc tys =
+  partitionByList (map isInvisibleArgFlag $ tyConArgFlags tc tys) tys
+
+-- | Given a list of things paired with their visibilities, partition the
+-- things into (invisible things, visible things).
+partitionInvisibles :: [(a, ArgFlag)] -> ([a], [a])
+partitionInvisibles = partitionWith pick_invis
+  where
+    pick_invis :: (a, ArgFlag) -> Either a a
+    pick_invis (thing, vis) | isInvisibleArgFlag vis = Left thing
+                            | otherwise              = Right thing
 
--- | Given a tycon and a list of things (which correspond to arguments),
--- partitions the things into
---      Inferred or Specified ones and
---      Required ones
--- The callback function is necessary for this scenario:
+-- | Given a 'TyCon' and a list of argument types to which the 'TyCon' is
+-- applied, determine each argument's visibility
+-- ('Inferred', 'Specified', or 'Required').
+--
+-- Wrinkle: consider the following scenario:
 --
 -- > T :: forall k. k -> k
--- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
+-- > tyConArgFlags T [forall m. m -> m -> m, S, R, Q]
 --
 -- After substituting, we get
 --
@@ -1568,23 +1590,38 @@ partitionInvisibleTypes tc tys = partitionInvisibles tc id tys
 --
 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
 -- and @Q@ is visible.
+tyConArgFlags :: TyCon -> [Type] -> [ArgFlag]
+tyConArgFlags tc = fun_kind_arg_flags (tyConKind tc)
+
+-- | Given a 'Type' and a list of argument types to which the 'Type' is
+-- applied, determine each argument's visibility
+-- ('Inferred', 'Specified', or 'Required').
 --
--- If you're absolutely sure that your tycon's kind doesn't end in a variable,
--- it's OK if the callback function panics, as that's the only time it's
--- consulted.
-partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
-partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
+-- Most of the time, the arguments will be 'Required', but not always. Consider
+-- @f :: forall a. a -> Type@. In @f Type Bool@, the first argument (@Type@) is
+-- '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).
+appTyArgFlags :: Type -> [Type] -> [ArgFlag]
+appTyArgFlags ty = fun_kind_arg_flags (typeKind ty)
+
+-- | Given a function kind and a list of argument types (where each argument's
+-- kind aligns with the corresponding position in the argument kind), determine
+-- each argument's visibility ('Inferred', 'Specified', or 'Required').
+fun_kind_arg_flags :: Kind -> [Type] -> [ArgFlag]
+fun_kind_arg_flags = go emptyTCvSubst
   where
-    go _ _ [] = ([], [])
-    go subst (ForAllTy (Bndr tv vis) res_ki) (x:xs)
-      | isVisibleArgFlag vis = second (x :) (go subst' res_ki xs)
-      | otherwise            = first  (x :) (go subst' res_ki xs)
+    go _ _ [] = []
+    go subst (ForAllTy (Bndr tv argf) res_ki) (arg_ty:arg_tys)
+      = argf : go subst' res_ki arg_tys
       where
-        subst' = extendTCvSubst subst tv (get_ty x)
-    go subst (TyVarTy tv) xs
-      | Just ki <- lookupTyVar subst tv = go subst ki xs
-    go _ _ xs = ([], xs)  -- something is ill-kinded. But this can happen
-                          -- when printing errors. Assume everything is visible.
+        subst' = extendTvSubst subst tv arg_ty
+    go subst (TyVarTy tv) arg_tys
+      | Just ki <- lookupTyVar subst tv = go subst ki arg_tys
+    go _ _ arg_tys = map (const Required) arg_tys
+                        -- something is ill-kinded. But this can happen
+                        -- when printing errors. Assume everything is Required.
 
 -- @isTauTy@ tests if a type has no foralls
 isTauTy :: Type -> Bool
@@ -1658,6 +1695,36 @@ caseBinder (Anon t)  _ d = d t
 
 Predicates on PredType
 
+Note [Types for coercions, predicates, and evidence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We treat differently:
+
+  (a) Predicate types
+        Test: isPredTy
+        Binders: DictIds
+        Kind: Constraint
+        Examples: (Eq a), and (a ~ b)
+
+  (b) Coercion types are primitive, unboxed equalities
+        Test: isCoVarTy
+        Binders: CoVars (can appear in coercions)
+        Kind: TYPE (TupleRep [])
+        Examples: (t1 ~# t2) or (t1 ~R# t2)
+
+  (c) Evidence types is the type of evidence manipulated by
+      the type constraint solver.
+        Test: isEvVarType
+        Binders: EvVars
+        Kind: Constraint or TYPE (TupleRep [])
+        Examples: all coercion types and predicate types
+
+Coercion types and predicate types are mutually exclusive,
+but evidence types are a superset of both.
+
+When treated as a user type, predicates are invisible and are
+implicitly instantiated; but coercion types, and non-pred evidence
+types, are just regular old types.
+
 Note [isPredTy complications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 You would think that we could define
@@ -1678,6 +1745,19 @@ But there are a number of complications:
   print it as such. But that means that isPredTy must return True for
   (C a => C [a]).  Admittedly that type is illegal in Haskell, but we
   want to print it nicely in error messages.
+
+Note [Evidence for quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The superclass mechanism in TcCanonical.makeSuperClasses risks
+taking a quantified constraint like
+   (forall a. C a => a ~ b)
+and generate superclass evidence
+   (forall a. C a => a ~# b)
+
+This is a funny thing: neither isPredTy nor isCoVarType are true
+of it.  So we are careful not to generate it in the first place:
+see Note [Equality superclasses in quantified constraints]
+in TcCanonical.
 -}
 
 -- | Split a type constructor application into its type constructor and
@@ -1730,16 +1810,39 @@ tcReturnsConstraintKind (FunTy    _ ty) = tcReturnsConstraintKind ty
 tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
 tcReturnsConstraintKind _               = False
 
+isEvVarType :: Type -> Bool
+-- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
+--         (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
+-- See Note [Types for coercions, predicates, and evidence]
+-- See Note [Evidence for quantified constraints]
+isEvVarType ty = isCoVarType ty || isPredTy ty
+
+-- | Does this type classify a core (unlifted) Coercion?
+-- At either role nominal or representational
+--    (t1 ~# t2) or (t1 ~R# t2)
+-- See Note [Types for coercions, predicates, and evidence]
+isCoVarType :: Type -> Bool
+isCoVarType ty
+  | Just (tc,tys) <- splitTyConApp_maybe ty
+  , (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
+  , tys `lengthIs` 4
+  = True
+isCoVarType _ = False
+
 -- | Is the type suitable to classify a given/wanted in the typechecker?
 isPredTy :: Type -> Bool
 -- See Note [isPredTy complications]
+-- NB: /not/ true of (t1 ~# t2) or (t1 ~R# t2)
+--     See Note [Types for coercions, predicates, and evidence]
 isPredTy ty = go ty []
   where
     go :: Type -> [KindOrType] -> Bool
+    -- Since we are looking at the kind,
+    -- no need to look through type synonyms
     go (AppTy ty1 ty2)   args       = go ty1 (ty2 : args)
     go (TyVarTy tv)      args       = go_k (tyVarKind tv) args
     go (TyConApp tc tys) args       = ASSERT( null args )  -- TyConApp invariant
-                                      go_tc tc tys
+                                      go_k (tyConKind tc) tys
     go (FunTy arg res) []
       | isPredTy arg                = isPredTy res   -- (Eq a => C a)
       | otherwise                   = False          -- (Int -> Bool)
@@ -1747,14 +1850,6 @@ isPredTy ty = go ty []
     go (CastTy _ co) args           = go_k (pSnd (coercionKind co)) args
     go _ _ = False
 
-    go_tc :: TyCon -> [KindOrType] -> Bool
-    go_tc tc args
-      | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
-                  = args `lengthIs` 4  -- ~# and ~R# sadly have result kind #
-                                       -- not Constraint; but we still want
-                                       -- isPredTy to reply True.
-      | otherwise = go_k (tyConKind tc) args
-
     go_k :: Kind -> [KindOrType] -> Bool
     -- True <=> ('k' applied to 'kts') = Constraint
     go_k k [] = tcIsConstraintKind k
@@ -2832,7 +2927,7 @@ splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
 
     invisible vs = Pair vs emptyVarSet
 
-    go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
+    go_tc tc tys = let (invis, vis) = partitionInvisibleTypes tc tys in
                    invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
 
 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet