#11638 closed feature request (duplicate)

referring to the existential type from a GADT pattern match with a type application

Reported by: rwbarton Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11387 Differential Rev(s):
Wiki Page:

Description

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 type a 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 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.

Change History (2)

comment:1 Changed 19 months ago by goldfire

I actually implemented this partially. But there are devilish details (numbered only for reference):

  1. We only pattern-match on existentials, never universals. That is, if we have
data T1 a where
  MkT1 :: a -> b -> T1 a

Using MkT1 as an expression: we could say MkT1 @Int @Bool 5 True. But as a pattern, we would have to omit the first argument: foo (MkT1 @b x y). This is confusing. I suppose we could include the universals in the pattern-match, but they would have to be underscores or an exact match for the inferred instantiation of the universal type variable.

  1. Users can reorder the variables in a data constructor, making point (1) even worse:
data T2 a where
  MkT2 :: forall b a. a -> b -> T2 a

Note the explicit forall reordering the variables. So it's not necessarily a prefix of variables that get dropped.

  1. Naturally, any visible type patterns would have to bind only bare type variables, never match against types. Otherwise, we've lost type erasure and parametricity.
  1. Do visible type patterns extend beyond data constructors? To wit:
foo :: forall a. a -> a
foo @b x = (x :: b)

Is that accepted? What about

(\ @a x -> (x :: a)) :: forall b. b -> b

It sure would be nice to be able to do this -- it would make continuation-passing style with fancy types easier.

There are solutions here, of course, but I just wanted to write down a few thoughts while I still remember them.

comment:2 Changed 16 months ago by goldfire

Resolution: duplicate
Status: newclosed

This is subsumed by #11350.

Note: See TracTickets for help on using tickets.