referring to the existential type from a GADT pattern match with a type application
Currently I can define a GADT like
data T where
MkT :: forall a. (Num a, Show a) => T
but it's useless on two counts:
- At a use of the constructor
MkT
, I can't specify what typea
I want to pack dictionaries for. (In fact the declaration is an error unless either the constraints are defaultable (as in the case above) or AllowAmbiguousTypes is enabled.) - At a pattern match against
MkT
, I have no way to refer to the type for which dictionaries were packed.
The solution is to add a field of type Proxy a
(possibly strict/unpacked) or Proxy# a
to MkT
. But these options are all a bit verbose and each have minor drawbacks.
I had hoped that TypeApplications would address the two points above directly.
- At a use of the constructor
MkT
, specify the type with a type applicationMkT @a
. This part works as of 90f35612. - At a pattern match against
MkT
, I would like to be able to match the type directly like this:
f :: T -> String
f t = case t of
MkT @a -> show (0 :: a)
This is the feature request.
Note that, while this may be stressful for the parser due to as-patterns, I don't think there is any actual ambiguity as long as (1) type applications only appear on constructors, not variables, and (2) all type applications appear before any value-level fields of the constructor.
Trac metadata
Trac field | Value |
---|---|
Version | 8.1 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |