[GHC] #13848: Unexpected order of variable quantification with GADT constructor
GHC
ghc-devs at haskell.org
Mon Jun 19 23:30:55 UTC 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:/compiler/typecheck/TcTyClsDecls.hs#l1855
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
More information about the ghc-tickets
mailing list