Re: [GHC] #11638: referring to the existential type from a GADT pattern match with a type application

24 Feb 2016

      #11638: referring to the existential type from a GADT pattern match with a type
application
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |             Keywords:
      Resolution:                    |  TypeApplications
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:                    |
-------------------------------------+-------------------------------------

Comment (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

 {{{#!hs
 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.

 2. Users can reorder the variables in a data constructor, making point (1)
 even worse:

 {{{#!hs
 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.

 3. 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.

 4. Do visible type patterns extend beyond data constructors? To wit:

 {{{#!hs
 foo :: forall a. a -> a
 foo @b x = (x :: b)
 }}}

     Is that accepted? What about

 {{{#!hs
 (\ @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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11638#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler