Skip to content

Core Lint error on 9.0.1+ (Inhomogeneous axiom)

The following program produces a Core Lint error on GHC 9.0.1 or later:

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

import Data.Kind
import Data.Proxy

type T :: forall (a :: Type) -> Constraint
class T a where
  f :: Proxy a
$ ~/Software/ghc-9.2.1-alpha1/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of TcGblEnv axioms ***
Bug.hs:10:1: warning:
    Inhomogeneous axiom
      lhs: T :: forall a -> Constraint
      rhs: Proxy :: * -> *
    In the coercion axiom N:T :: []. T ~_R Proxy
    Substitution: [TCvSubst
                     In scope: InScope {}
                     Type env: []
                     Co env: []]
*** Offending Program ***
axiom N:T :: T = Proxy -- Defined at Bug.hs:10:1
*** End of Offense ***


<no location info>: error: 
Compilation had errors

This appears to be a regression from GHC 8.10.4, which does not trigger the same Core Lint error.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information