GitLab

Here are two files:

-- Lib.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Lib where

import Data.Kind

class C (f :: k -> Type) z where
  type T (x :: f a) :: f a

-- App.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module App where

import Data.Kind
import Data.Proxy
import Lib

type family F (x :: Proxy a) :: Proxy a
instance C Proxy z where
  type T x = F x

Compiling this with GHC 8.8.1 passes Core Lint:

$ /opt/ghc/8.8.1/bin/ghc -c Lib.hs && /opt/ghc/8.8.1/bin/ghc -c App.hs -dcore-lint

But it does not pass Core Lint on GHC 8.10.1-alpha1:

$ /opt/ghc/8.10.1/bin/ghc -c Lib.hs && /opt/ghc/8.10.1/bin/ghc -c App.hs -dcore-lint
ghc: panic! (the 'impossible' happened)
  (GHC version 8.10.0.20191122:
        Core Lint error
  <no location info>: warning:
      The variable @ k1_aiz is out of scope
      Substitution: [TCvSubst
                       In scope: InScope {}
                       Type env: []
                       Co env: []]
  T
  [TCvSubst
     In scope: InScope {k1_aiz a_awk x_awl}
     Type env: [aig :-> x_awl, awg :-> a_awk]
     Co env: []]
  [a_awk, x_awl]
  []
  [k1_aiz, Proxy, a_awk, x_awl]
  F x_awl
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/FamInst.hs:184:31 in ghc:FamInst

---

Another curious thing is that if you load Lib.hs into GHCi, you'll observe something strange about the kind of T:

$ /opt/ghc/8.10.1/bin/ghci Lib.hs
GHCi, version 8.10.0.20191122: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Lib              ( Lib.hs, interpreted )
Ok, one module loaded.
λ> :i T
type C :: forall k k1. (k1 -> *) -> k -> Constraint
class C f z where
  type T :: forall k2 (f :: k1 -> *) (a :: k2). f a -> f a
  type family T x
        -- Defined at Lib.hs:11:3

Note that T has kind forall k2 (f :: k1 -> *) (a :: k2). f a -> f a, which does not appear to be well kinded. It's unclear to me if this is the cause behind the Core Lint error or not.