Re: [GHC] #13848: Unexpected order of variable quantification with GADT constructor

19 Jun 2017

      #13848: Unexpected order of variable quantification with GADT constructor
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |             Keywords:
      Resolution:                    |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Above, I implied that GHC was inferring the topological order for `a` and
 `n` in the type signature for `VCons` even with an explicit `forall`. I
 just realized there's more to it after reading `Note [mkGADTVars]`.
 [http://git.haskell.org/ghc.git/blob/5c93df90a96494229b60bbed0971a4b08c0326a6...
 The relevant excerpt]:

 {{{
 Note [mkGADTVars]
 ~~~~~~~~~~~~~~~~~

 Running example:

 data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
   MkT :: T x1 * (Proxy (y :: x1), z) z

 We need the rejigged type to be

   MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2).
          forall (y :: x1) (z :: *).
          (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z)
       => T x1 k2 a b

 You might naively expect that z should become a universal tyvar,
 not an existential. (After all, x1 becomes a universal tyvar.)
 The problem is that the universal tyvars must have exactly the
 same kinds as the tyConTyVars. z has kind * while b has kind k2.
 So we need an existential tyvar and a heterogeneous equality
 constraint.
 }}}

 So what's //really// going on is that GHC is putting all of the
 universally quantified variables (`a`) before the existentially quantified
 ones (`n`).

 Still, I still think that GHC ought to adhere to what the user wrote if
 they bother to write an explicit `forall`, because otherwise you have to
 trace out the variable order that GHC happens to infer.

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