Core Lint error (ghc 9.1.0.20201202)
This piece of code (see #19092 (closed)) triggers a core lint error, I don't know why!
{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}
{-# Options_GHC -dcore-lint #-}
import Data.Type.Equality
import Data.Kind
type PolyKinded :: Type -> Type
type PolyKinded res = (forall (k :: Type). k -> res)
infix 4
===
type
(===) :: PolyKinded (PolyKinded Bool)
type family
a === b where
a === a = True
_ === _ = False
type TryUnify :: Bool -> PolyKinded (PolyKinded Constraint)
class (a === b) ~ cond
=> TryUnify cond a b
$ ghc --interactive -ignore-dot-ghci ~/hs/4007_bug.hs
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/4007_bug.hs, interpreted )
*** Core Lint errors : in result of TcGblEnv axioms ***
/home/baldur/hs/4007_bug.hs:22:1: warning:
Kind application error in type `TryUnify cond_aBb a_aBc b_aBd'
Function kind = Bool -> forall k. k -> forall k. k -> Constraint
Arg types = [cond_aBb, k2_X0, a_aBc, k2_X0, b_aBd]
Fun: k2_X0 -> forall k. k -> Constraint
a_aBc :: k1_aBi
In the coercion axiom N:TryUnify :: [(cond_aBb :: Bool), k1_aBi,
(a_aBc :: k1_aBi), k2_aBi, (b_aBd :: k2_aBi)].
TryUnify cond_aBb a_aBc b_aBd
~_R
(a_aBc === b_aBd) ~ cond_aBb
Substitution: [TCvSubst
In scope: InScope {k2_X0 cond_aBb a_aBc b_aBd k1_aBi}
Type env: [aBb :-> cond_aBb, aBc :-> a_aBc, aBd :-> b_aBd,
aBi :-> k2_X0]
Co env: []]
/home/baldur/hs/4007_bug.hs:22:1: warning:
Kind application error in type `a_aBc === b_aBd'
Function kind = forall k. k -> forall k. k -> Bool
Arg types = [k2_X0, a_aBc, k2_X0, b_aBd]
Fun: k2_X0 -> forall k. k -> Bool
a_aBc :: k1_aBi
In the coercion axiom N:TryUnify :: [(cond_aBb :: Bool), k1_aBi,
(a_aBc :: k1_aBi), k2_aBi, (b_aBd :: k2_aBi)].
TryUnify cond_aBb a_aBc b_aBd
~_R
(a_aBc === b_aBd) ~ cond_aBb
Substitution: [TCvSubst
In scope: InScope {k2_X0 cond_aBb a_aBc b_aBd k1_aBi}
Type env: [aBb :-> cond_aBb, aBc :-> a_aBc, aBd :-> b_aBd,
aBi :-> k2_X0]
Co env: []]
*** Offending Program ***
axiom D:R:=== ::
forall {k} {a :: k}.
a === a = 'True -- Defined at /home/baldur/hs/4007_bug.hs:18:2
_ === _ = 'False -- Defined at /home/baldur/hs/4007_bug.hs:19:2
axiom N:TryUnify ::
forall {cond :: Bool} {k1} {a :: k1} {k2} {b :: k2}.
TryUnify cond a b = (a_aBc === b_aBd) ~ cond_aBb
-- Defined at /home/baldur/hs/4007_bug.hs:22:1
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
ghci>
If you unfold
type TryUnify :: Bool -> PolyKinded (PolyKinded Constraint)
PolyKinded
the program compiles
type TryUnify :: Bool -> forall k. k -> PolyKinded Constraint
type TryUnify :: Bool -> forall k. k -> forall j. j -> Constraint