Strange interaction between higher-rank kinds and type synonyms

Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind

data family Sing (a :: k)

data (a :: j) :~~: (b :: k) where
  HRefl :: a :~~: a

data instance Sing (z :: a :~~: b) where
  SHRefl :: Sing HRefl

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
             Sing r
          -> p HRefl
          -> p r
(%:~~:->) SHRefl pHRefl = pHRefl

type App f x = f x
type HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x

Now I want to refactor this so that I use App:

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
             Sing r
          -> App p HRefl
          -> App p r

However, GHC doesn't like that:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:21:20: error:
    • Expected kind ‘(:~~:) j z a a’,
        but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’
    • In the second argument of ‘App’, namely ‘HRefl’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> App p HRefl -> App p r
   |
21 |           -> App p HRefl
   |                    ^^^^^

Bug.hs:22:20: error:
    • Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’
    • In the second argument of ‘App’, namely ‘r’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> App p HRefl -> App p r
   |
22 |           -> App p r
   |                    ^

These errors are surprising to me, since it appears that the two higher-rank types, z and y, are behaving differently here: y appears to be willing to unify with other types in applications of p, but z isn't! I would expect //both// to be willing to unify in applications of p.

Out of desperation, I tried this other formulation of (%:~~:->) which uses HRApp instead of App:

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
             Sing r
          -> HRApp p HRefl
          -> HRApp p r

But now I get an even stranger error message:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:21:20: error:
    • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
        but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
    • In the first argument of ‘HRApp’, namely ‘p’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> HRApp p HRefl -> HRApp p r
   |
21 |           -> HRApp p HRefl
   |                    ^

Bug.hs:21:20: error:
    • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
        but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
    • In the first argument of ‘HRApp’, namely ‘p’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> HRApp p HRefl -> HRApp p r
   |
21 |           -> HRApp p HRefl
   |                    ^

Bug.hs:22:20: error:
    • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
        but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
    • In the first argument of ‘HRApp’, namely ‘p’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> HRApp p HRefl -> HRApp p r
   |
22 |           -> HRApp p r
   |                    ^

That's right, it can't match the kinds:

• forall z (y :: z). (:~~:) j z a y -> *, and
• forall z (y :: z). (:~~:) j z a y -> *

Uh... what? Those are the same kind!

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture