Skip to content

Core Lint error with a type family

The following program fails Core Lint

{-# LANGUAGE TypeFamilies #-}
module M where

import Data.Kind (Type)

data MP1 a = MP1 a

type family Fixup (f :: Type) (g :: Type) :: Type where
  Fixup f (MP1 f) = MP1 f
  Fixup f f = f
*** Core Lint errors : in result of TcGblEnv axioms ***
M.hs:8:13: warning:
    Incorrect incompatible branch: CoAxBranch (M.hs:9:3-25): [f_aw2,
                                                              MP1 f_aw2] => MP1 f_aw2
    In the coercion axiom D:R:Fixup :: {[f_aw2].
                                        Fixup f_aw2 (MP1 f_aw2)
                                        ~_N
                                        MP1 f_aw2
                                        [f_aw3]. Fixup f_aw3 f_aw3 ~_N f_aw3}

Credit to @alt-romes for finding this issue in linear-base; I've only minimized it.

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