Incorrect type variable on the LHS of injectivity condition [GHC-88333]

This error occurs when the variable on the left-hand side of an injectivity annotation is not the type family’s result variable.

Type families in Haskell define type-level functions. In type family F a = r | r -> a, the injectivity annotation | r -> a states that the result type r uniquely determines the input type a: equal results imply equal inputs. The left-hand side must be the result variable r named after =, and the right-hand side lists the input variables determined by that result.

Examples

Incorrect type variable on the LHS of injectivity condition

In the example, the associated type family Ft is defined with an incorrect injectivity annotation. The left-hand side (LHS) of the injectivity condition should be the output type variable (r), but in the definition, it is the input type variable (a). This is what the error message is referring to.

Test.hs

Before

module IncorrectTypeVarLHSInjectivityCondition where

class Fcl a where
  type Ft a = r | a -> a

After

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module IncorrectTypeVarLHSInjectivityCondition where

class Fcl a where
  type Ft a = r | r -> a

Incorrect type variable on the LHS of injectivity condition

In the example, type family Fc is defined with an incorrect injectivity annotation. The left-hand side (LHS) of the injectivity condition should be the output type variable (r), but in the definition, it is the input type variable (a). This is what the error message is referring to.

Test.hs

Before

module IncorrectTypeVarLHSInjectivityCondition where

type family Fc a = r | a -> a where
  Fc a = a

After

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module IncorrectTypeVarLHSInjectivityCondition where

type family Fc a = r | r -> a where
  Fc a = a

Incorrect type variable on the LHS of injectivity condition

In the example, type family F is defined with an incorrect injectivity annotation. The left-hand side (LHS) of the injectivity condition should be the output type variable (r), but in the definition, it is the input type variable (a). This is what the error message is referring to.

Test.hs

Before

module IncorrectTypeVarLHSInjectivityCondition where

type family F a = r | a -> a

After

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module IncorrectTypeVarLHSInjectivityCondition where

type family F a = r | r -> a