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?
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With