Skip to content

Unable to deduce simple equality?

I would expect the following program to typecheck, but it doesn't:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
module Bug where

import Data.Kind
import Data.Type.Equality

eq :: F Int :~: G Int
eq = Refl

type F = G
type family G :: Type ~> Type
$ ~/Software/ghc-kcsongor/inplace/bin/ghc-stage2 Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:6: error:
    • Couldn't match type ‘G Int’ with ‘G Int’
      Expected type: (:~:) @{*} (F Int) (G Int)
        Actual type: (:~:) @{*} (G Int) (G Int)
      NB: ‘G’ is a non-injective type family
    • In the expression: Refl
      In an equation for ‘eq’: eq = Refl
   |
11 | eq = Refl
   |      ^^^^