GitLab

The following program simply errors with GHC 8.6.4:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where

import Data.Kind

data SameKind :: forall k. k -> k -> Type

f :: forall a k (b :: k). SameKind a b -> ()
f = g
  where
    g :: SameKind a b -> ()
    g _ = ()

$ /opt/ghc/8.6.4/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:9:6: error:
    • These kind and type variables: a k (b :: k)
      are out of dependency order. Perhaps try this ordering:
        k (a :: k) (b :: k)
    • In the type signature:
        f :: forall a k (b :: k). SameKind a b -> ()
  |
9 | f :: forall a k (b :: k). SameKind a b -> ()
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

On GHC HEAD, however, it throws a GHC internal error:

GHCi, version 8.9.20190309: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:9:6: error:
    • These kind and type variables: a k (b :: k)
      are out of dependency order. Perhaps try this ordering:
        k (a :: k) (b :: k)
    • In the type signature:
        f :: forall a k (b :: k). SameKind a b -> ()
  |
9 | f :: forall a k (b :: k). SameKind a b -> ()
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:12:19: error:
    • GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: []
    • In the first argument of ‘SameKind’, namely ‘a’
      In the type signature: g :: SameKind a b -> ()
      In an equation for ‘f’:
          f = g
            where
                g :: SameKind a b -> ()
                g _ = ()
   |
12 |     g :: SameKind a b -> ()
   |                   ^