Various FUN-related oddities

While trying out FUN recently, I noticed some warts:

1. The documentation for funTyCon (which describes FUN) appears to be incorrect:

   -- | The @FUN@ type constructor.
   --
   -- @
   -- FUN :: forall {m :: Multiplicity} {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
   --         TYPE rep1 -> TYPE rep2 -> *
   -- @
   --
   -- The runtime representations quantification is left inferred. This
   -- means they cannot be specified with @-XTypeApplications@.
   --
   -- This is a deliberate choice to allow future extensions to the
   -- function arrow. To allow visible application a type synonym can be
   -- defined:
   --
   -- @
   -- type Arr :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep).
   --             TYPE rep1 -> TYPE rep2 -> Type
   -- type Arr = FUN
   -- @
   --
   funTyCon :: TyCon
   funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
     where
       -- See also unrestrictedFunTyCon
       tc_bndrs = [ mkNamedTyConBinder Required multiplicityTyVar
                  , mkNamedTyConBinder Inferred runtimeRep1TyVar
                  , mkNamedTyConBinder Inferred runtimeRep2TyVar ]
                  ++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty
                                                , tYPE runtimeRep2Ty
                                                ]
       tc_rep_nm = mkPrelTyConRepName funTyConName

   The kind FUN given above is different than what it is according to GHCi:

   λ> :set -fprint-explicit-foralls -fprint-explicit-runtime-reps
   λ> import GHC.Exts
   λ> :kind FUN
   FUN :: forall (n :: GHC.Types.Multiplicity) ->
          forall {q :: RuntimeRep} {r :: RuntimeRep}.
          TYPE q -> TYPE r -> *

   Here, the Multiplicity type variable binder is required, not inferred.

2. Related to (1), is there any reason that the Multiplicity argument needs to be named? Would it not suffice to use mkAnonTyConBinder instead so that the kind is this?

   FUN :: forall {q :: RuntimeRep} {r :: RuntimeRep}.
          Multiplicity -> TYPE q -> TYPE r -> *

   As far as I can tell, the n type variable is not actually used anywhere.

3. If you reify FUN with Template Haskell, you'll get this:

   λ> :set -XTemplateHaskell
   λ> :m + GHC.Exts Language.Haskell.TH
   λ> putStrLn $(reify ''FUN >>= stringE . show)
   PrimTyConI GHC.Prim.FUN 2 False

   This claims that there are 2 visible type arguments, but in reality, there are 3.

4. FUN appears to bypass the need to enable LinearTypes. For example, the following typechecks even though LinearTypes is not enabled:

   {-# LANGUAGE DataKinds #-}
   module Bug where
   
   import Data.Kind
   import GHC.Types
   
   f :: FUN One a a
   f x = x

cc @monoidal