Why does `forall (a :: j) (b:: k)` work differently than `forall (p :: (j,k))`?

Question

I'm trying to understand the difference between using forall to quantify two type variables and using forall to quantify a single type variable of tuple kind.

For example, given the following type families:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}

type family Fst (p :: (a,b)) :: a where
  Fst '(a,_) = a
type family Snd (p :: (a,b)) :: b where
  Snd '(_,b) = b
type family Pair (p :: (Type,Type)) :: Type where
  Pair '(a,b) = (a,b)

I can define an identity on pairs using two type variables, and get it to compile on GHC 8.0.1:

ex0 :: forall (a :: Type) (b :: Type). Pair '(a,b) -> (Fst '(a,b), Snd '(a,b))
ex0 = id

The same definition doesn't compile if I use a single type variable of tuple kind, however:

ex1 :: forall (p :: (Type,Type)). Pair p -> (Fst p, Snd p)
ex1 = id
-- Ex.hs:20:7: error:
--     • Couldn't match type ‘Pair p’ with ‘(Fst p, Snd p)’
--       Expected type: Pair p -> (Fst p, Snd p)
--         Actual type: (Fst p, Snd p) -> (Fst p, Snd p)
--     • In the expression: id
--       In an equation for ‘ex1’: ex1 = id
--     • Relevant bindings include
--         ex1 :: Pair p -> (Fst p, Snd p) (bound at Ex.hs:20:1)

Is the problem that p might be ⊥?

Ionian

Answer 1

The reason is simply that there is no eta-conversion checking on the type-level. To begin with, there is no mechanism for distinguishing data definitions from single-constructor records/products which possibly have eta laws. I don't think p possibly being ⊥ is a valid reason for this. Even in partial lazy languages, eta equality for pairs holds (w.r.t. observational equivalence).

Cherokee

Answer 2

Is the problem that p might be ⊥?

More or less. Unfortunately, all kinds are inhabited by the empty type family.

type family Any :: k

Which frustrates any theory which would allow what you are trying to do. I think it really needs to be fixed; I'm not sure if there are any plans to do so, however.

Venezuela

Any should not be an issue. If GHC translated matching on type-level records to primitive projections, as in Agda/Coq, then Any would be indistinguishable from (Fst Any, Snd Any), validating an eta rule. – Basis

@AndrásKovács, ah I see what you mean. I think Any is still relevant as it poses a problem for coproducts -- or e.g. if (,) were defined as a data type in Agda instead of a record. – Venezuela

yeah, I meant it's not a problem in this case, but I think it's also not really a problem for coproducts, because although Any invalidates coproduct eta, type checkers pretty much never check for coproduct eta anyway. (But I also think getting rid of Any would be good). – Basis

@AndrásKovács, yes but in Agda, with no type-level bottoms (or any bottoms) there is at least the possibility of pattern matching so that you can convince your definition to pass. Not so in Haskell. But the more we talk the less relevant to this precise question my comment seems, and it's just a general grievance of mine. :-p – Venezuela