Why can't constructors have required type arguments?

Question

Let's say I define the following datatype:

data fmt :* (n :: Nat) where
    Rep :: fmt -> fmt :* n

Using RequiredTypeArguments, I can define a function that takes the n parameter as a required type argument:

(*:) :: fmt -> forall n -> fmt :* n
fmt *: n = Rep fmt

But if I try to do this directly in the datatype constructor, I get an error from GHC 9.10.1:

data a :* (n :: Nat) where
    (:*) :: a -> forall n -> a :* n

    • Illegal visible, dependent quantification in the type of a term
    • In the definition of data constructor ‘:*’
   |
83 |     (:*) :: a -> forall n -> a :* n
   |                  ^^^^^^^^^^^^^^^^^^

What makes (:*) be problematic vis-a-vis (*:)? What would break / what would be undecidable during typechecking if GHC accepted it?

Answer 1

Disclaimer: I'm not sure if this is the true motivation, but it seems like one possible motivation.

If I could write 'a' :* 3 and 'b' :* 5, I think I'd expect to also be able to write something like

case x of
    'a' :* 3 -> ...
    'b' :* 5 -> ...
    _ -> ...

That seems problematic given that at runtime, 3 and 5 don't actually exist anywhere as chunks of data.