Skip to content

Rank 2 InstanceSig that involves a non-injective type family gets rejected despite being identical

Summary

When given an instance signature that is rank 2 and contains a non-injective type family, the compiler rejects the signature as being "more general" despite being, AFAICT, identical. This problem seems to be caused by the intersection of those three features; it disappears when removing any of them:

  • bringing the function back down to rank 1 by using a newtype wrapper fixes this
  • removing the non-injective type family from the signature
  • removing the instance signature

Steps to reproduce

Here's a small example. I haven't managed to make it smaller since it needs all three features.

#! ghc-9.2.7 -package mtl

{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE Haskell2010         #-}
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}

import Control.Monad.Identity

type family HKD f a where
  HKD Identity a = a
  HKD f        a = f a

type FFunction f g = forall a. HKD f a -> HKD g a

class FFunctor t where
  ffmap :: forall f g. FFunction f g -> t f -> t g

data A f = A (HKD f Int)

instance FFunctor A where
  ffmap :: forall f g. FFunction f g -> A f -> A g
  ffmap f (A x) = A (f @Int x)

Expected behavior

AFAICT, this should compile, since the type given in the instance sig is correct, and the same file compiles if the instance sig is removed?

Environment

  • GHC version used: 9.2.7
Edited by Antoine Leblanc
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information