Re: [GHC] #14288: ScopedTypeVariables with nested foralls broken since 8.0.2

29 Sep 2017

      #14288: ScopedTypeVariables with nested foralls broken since 8.0.2
-------------------------------------+-------------------------------------
        Reporter:  MikolajKonarski   |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Linux             |         Architecture:  x86_64
 Type of failure:  GHC rejects       |  (amd64)
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I'm worried that this design decision will come back to bite us once the
 [https://github.com/ghc-proposals/ghc-
 proposals/blob/dbf516088d2839432c9568c3d1f7ae28d46aeb43/proposals/0005
 -bidir-constr-sigs.rst pattern synonym construction function signatures]
 proposal is implemented. To recap, if you have an explicitly bidirectional
 pattern synonym like:

 {{{#!hs
 data T a where
   MkT :: forall a b. (Show b) => a -> b -> T a

 pattern ExNumPat :: forall a. (Num a, Eq a) => forall b. (Show b) => b ->
 T a
 pattern ExNumPat x <- MkT 42 x where
   ExNumPat x = MkT 42 x
 }}}

 Then this proposal would allow you to write an explicit type signature for
 the builder expression, like so:

 {{{#!hs
 pattern ExNumPat :: forall a. (Num a, Eq a) => forall b. (Show b) => b ->
 T a
 pattern ExNumPat x <- MkT 42 x where
   ExNumPat :: forall a. (Num a, Ord a) => forall b. (Show b) => b -> T a
   ExNumPat x = MkT 42 x
 }}}

 Where this type signature must be the same as the pattern signature save
 for the required constraints, which are allowed to be different.

 Once we gain the ability to write type signatures for builder expressions
 like this (and thus, the ability to lexically scope type variables with
 `-XScopedTypeVariables`), folks will naturally want to write builders with
 `-XTypeApplications` like this:

 {{{#!hs
   ExNumPat :: forall a. (Num a, Ord a) => forall b. (Show b) => b -> T a
   ExNumPat x = MkT @a @b 42 x
 }}}

 (This is a relatively simple example, but you could imagine this being
 more useful when fancier types are involved.)

 But there's a big problem here—. By the rules of `-XScopedTypeVariables`,
 only `a` will be in scope in the builder's RHS, not `b`! With normal
 function type signatures, you can work around this problem by just
 smashing `forall a. forall b` into `forall a b`, but with pattern
 synonyms, we cannot do this—the required type variables and the provided
 type variables //must// be quantified separately! So this design prevents
 us from writing pattern synonym builders that visibly apply provided type
 variables using `-XTypeApplications`.

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