Order of inferred quantification is observable
Background
In GHC, a forall-bound variable may have one of the three visibilities:
- required, written
forall a ->
- specified, written
forall a.
- inferred, written
forall {a}.
With type applications, it is easy to observe the order of specified variables. f @Int @Bool
means different things depending on whether we have:
f1 :: forall a b. (a, b) -> ...
f2 :: forall b a. (a, b) -> ... -- not the same!
However, the order of inferred variables is supposed to be unobservable by the programmer:
g1 :: forall {a} {b}. (a, b) -> ...
g2 :: forall {b} {a}. (a, b) -> ... -- indistinguishable from g1
Inferred variables are ignored by type applications for this reason.
Bug
I have constructed examples that allow the programmer to observe the order of inferred quantification.
Term-level example
Let us define const_inf1
and const_inf2
as follows:
const_inf1 :: () -> forall {a} {b}. a -> b -> a
const_inf2 :: () -> forall {b} {a}. a -> b -> a
const_inf1 _ x _ = x
const_inf2 _ x _ = x
We would like const_inf1
and const_inf2
to be interchangeable in all contexts. However, consider this definition:
const_spec :: () -> forall a b. a -> b -> a
const_spec = const_inf1
This is accepted by GHC, but if we replace const_inf1
with const_inf2
, the definition is rejected with the following error message:
• Couldn't match type ‘a’ with ‘b’
Expected: () -> forall a b. a -> b -> a
Actual: () -> forall {b} {a}. a -> b -> a
Interestingly enough, the type variables {a}
and {b}
are "inferred" only de jure; in the actual program, they are very much specified by an explicit forall
. In other words, their order is determined by the source code, not by implementation details of the compiler, so this is only mildly unsatisfactory. The situation is much worse at the type level.
Type-level example
Let us define D
as follows (no explicit signature):
data D a b
What kind does GHC infer for D
? There are two options:
D :: forall {k1} {k2}. k1 -> k2 -> Type
D :: forall {k2} {k1}. k1 -> k2 -> Type
This time, the choice between these options is determined by implementation details, so it is important to make sure that the order of quantification is not observable. We can define D1
and D2
with explicit signatures to aid the investigation:
type D1 :: forall {k1} {k2}. k1 -> k2 -> Type
type D2 :: forall {k2} {k1}. k1 -> k2 -> Type
data D1 a b
data D2 a b
Note that the kinds of D1
and D2
correspond to the possible inferred kinds for D
. So any program that can distinguish D
, D1
, and D2
, depends on GHC's implementation details. Behold:
type family F :: forall k1 k2. k1 -> k2 -> Type
type instance F = D1
This is accepted as long as we use D1
, but rejected if we use D2
with the following error:
• Couldn't match kind ‘k2’ with ‘k1’
Expected kind ‘forall k1 k2. k1 -> k2 -> Type’,
but ‘D2’ has kind ‘forall {k2} {k1}. k1 -> k2 -> Type’
Cause
The bug occurs when eqType
is used to compare types for equality, because eqType
and tcEqType
ignore the distinction between inferred and specified variables. This design decision is described in Note [ForAllTy and type equality]
:
Click to expand
{- Note [ForAllTy and type equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we compare (ForAllTy (Bndr tv1 vis1) ty1)
and (ForAllTy (Bndr tv2 vis2) ty2)
what should we do about `vis1` vs `vis2`.
First, we always compare with `eqForAllVis`.
But what decision do we make?
Should GHC type-check the following program (adapted from #15740)?
{-# LANGUAGE PolyKinds, ... #-}
data D a
type family F :: forall k. k -> Type
type instance F = D
Due to the way F is declared, any instance of F must have a right-hand side
whose kind is equal to `forall k. k -> Type`. The kind of D is
`forall {k}. k -> Type`, which is very close, but technically uses distinct
Core:
-----------------------------------------------------------
| Source Haskell | Core |
-----------------------------------------------------------
| forall k. <...> | ForAllTy (Bndr k Specified) (<...>) |
| forall {k}. <...> | ForAllTy (Bndr k Inferred) (<...>) |
-----------------------------------------------------------
We could deem these kinds to be unequal, but that would imply rejecting
programs like the one above. Whether a kind variable binder ends up being
specified or inferred can be somewhat subtle, however, especially for kinds
that aren't explicitly written out in the source code (like in D above).
For now, we decide
the specified/inferred status of an invisible type variable binder
does not affect GHC's notion of equality.
That is, we have the following:
--------------------------------------------------
| Type 1 | Type 2 | Equal? |
--------------------|-----------------------------
| forall k. <...> | forall k. <...> | Yes |
| | forall {k}. <...> | Yes |
| | forall k -> <...> | No |
--------------------------------------------------
| forall {k}. <...> | forall k. <...> | Yes |
| | forall {k}. <...> | Yes |
| | forall k -> <...> | No |
--------------------------------------------------
| forall k -> <...> | forall k. <...> | No |
| | forall {k}. <...> | No |
| | forall k -> <...> | Yes |
--------------------------------------------------
IMPORTANT NOTE: if we want to change this decision, ForAllCo will need to carry
visiblity (by taking a ForAllTyBinder rathre than a TyCoVar), so that
coercionLKind/RKind build forall types that match (are equal to) the desired
ones. Otherwise we get an infinite loop in the solver via canEqCanLHSHetero.
Examples: T16946, T15079.
As far as examples reported in this ticket are concerned, the following uses of tcEqType
are involved:
- In
uType
:defer ty1 ty2 -- See Note [Check for equality before deferring] | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1) | otherwise = uType_defer t_or_k origin ty1 ty2
- In
checkExpectedKind
:; if act_kind' `tcEqType` exp_kind then return res_ty -- This is very common else ...