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
| ^^^^