Several bugs with forall (cv::t1~#t2). ty)

In principle, GHC supports coercion variable in a forall-type. Thus a type can look like forall (cv:t1~#t2). body_ty, where body_ty can mention the coercion variable cv. See Note [Why ForAllTy can quantify over a coercion variable] in GHC.Core.TyCo.Rep.

But I discover that GHC has multiple bugs if you actually have any terms with such a type. Here are the four bugs I have found

• typeKind ty simply loops if given a type that quantifies over a coercion variable. (It's a trivial bug, easily fixed, but longstanding.)

• Core Lint (specifically lintCoArg) complains if it sees an application (f co) where f has type (forall (cv:t1~#t2). blah). (More usually f has type (t1~#t2)=>blah, when blah does not mention cv.)

• GHC.Core.Opt.Arity.typeArity/typeOneShots didn't count coercion arguments if the type was (forall cv. blah)

• GHC.Core.Opt.Simplify.Iteration.simpl_lam (which deals with bete-reduction) crashed when the function type looks like (forall cv. blah) and the application has a coercion argument.

I discovered this when working on !11492 which fixes #3781. When compiling base:Data/Typeable/Internal.hs the float-out pass yielded this function:

lvl_sjWn
  :: forall (r :: RuntimeRep) k1 (co['Many] :: k1 ~# TYPE r)
            (b :: k1) (r :: RuntimeRep) k2 k1 (a :: k1 -> k2).
     (a ~# (->) (b |> co), (k1 -> k2) ~# (TYPE r -> *)) =>
     TypeRep ((->) (b |> co)) -> TypeRep a -> Void
[LclId, Arity=5, Str=<L><L><L><L><L>b, Cpr=b]
lvl_sjWn
  = \ (@(r_a2ru :: RuntimeRep))
      (@k1_a2qV)
      (co_a2rv :: k1_a2qV ~# TYPE r_a2ru)
      (@(b_a2qX :: k1_a2qV))
      (@(r_a2rJ :: RuntimeRep))
      (@k2_a2qQ)
      (@k1_a2qP)
      (@(a_a2qR :: k1_a2qP -> k2_a2qQ))
      (co_a2gm :: a_a2qR ~# (->) (b_a2qX |> co_a2rv))
      (co_a2gl :: (k1_a2qP -> k2_a2qQ) ~# (TYPE r_a2rJ -> *))
      (a_sjPk :: TypeRep ((->) (b_a2qX |> co_a2rv)))
      (rep_a1ka :: TypeRep a_a2qR) ->
      raise#
        @'Lifted
        @LiftedRep
        @SomeException
        @Void
        (noinline
           @([Char] -> SomeException)
           errorCallException
           (augment
              @Char
              lvl_sjWi
              (augment
                 @Char
                 (\ (@b_ajEq)
                    (c_ajEr [OS=OneShot] :: Char -> b_ajEq -> b_ajEq)
                    (n_ajEs [OS=OneShot] :: b_ajEq) ->
                    foldr
                      @Char
                      @b_ajEq
                      c_ajEr
                      n_ajEs
                      (showTypeable
                         @(TYPE r_a2rJ -> *)
                         @((->) (b_a2qX |> co_a2rv))
                         lvl_sjWj
                         a_sjPk
                         ([] @Char)))
                 (augment
                    @Char
                    lvl_sjWl
                    (showTypeable
                       @(TYPE r_a2rJ -> *)
                       @((->) (b_a2qX |> co_a2rv))
                       lvl_sjWm
                       (rep_a1ka
                        `cast` ((TypeRep co_a2gl co_a2gm)_R
                                :: TypeRep a_a2qR ~R# TypeRep ((->) (b_a2qX |> co_a2rv))))
                       ([] @Char))))))

Somehow this has never happened before!