Various FUN-related oddities
While trying out FUN
recently, I noticed some warts:
-
The documentation for
funTyCon
(which describesFUN
) 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. -
Related to (1), is there any reason that the
Multiplicity
argument needs to be named? Would it not suffice to usemkAnonTyConBinder
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. -
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.
-
FUN
appears to bypass the need to enableLinearTypes
. For example, the following typechecks even thoughLinearTypes
is not enabled:{-# LANGUAGE DataKinds #-} module Bug where import Data.Kind import GHC.Types f :: FUN One a a f x = x
cc @monoidal