GHC 9.0 unable to deduce that instance signature is at least as general as class signature
The following program compiles OK on GHC 8.10 but not on GHC 9.0:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
-- base
import Data.Kind
( Constraint )
--------------------------------------------------------------------------------
data SplineType = Open | Closed
data Curve ( clo :: SplineType ) = Curve {- ... -}
data Spline ( clo :: SplineType ) = Spline {- ... -}
class KnownSplineType ( clo :: SplineType ) where
type TraversalCt clo ( clo' :: SplineType ) :: Constraint
biwitherSpline
:: ( forall clo'. ( TraversalCt clo clo' )
=> Curve clo' -> Maybe ( Curve clo' )
)
-> Spline clo
-> Maybe ( Spline clo )
instance KnownSplineType Open where
type TraversalCt Open clo' = clo' ~ Open
biwitherSpline
:: ( Curve Open -> Maybe ( Curve Open ) )
-> Spline Open
-> Maybe ( Spline Open )
biwitherSpline _ _ = undefined
With GHC 9.0, I get the following error:
Bug.hs:37:8: error:
* Couldn't match type: Curve 'Open -> Maybe (Curve 'Open)
with: forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo')
Expected: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo'))
-> Spline 'Open -> Maybe (Spline 'Open)
Actual: (Curve 'Open -> Maybe (Curve 'Open))
-> Spline 'Open -> Maybe (Spline 'Open)
* When checking that instance signature for `biwitherSpline'
is more general than its signature in the class
Instance sig: (Curve 'Open -> Maybe (Curve 'Open))
-> Spline 'Open -> Maybe (Spline 'Open)
Class sig: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo'))
-> Spline 'Open -> Maybe (Spline 'Open)
In the instance declaration for `KnownSplineType 'Open'
|
37 | :: ( Curve Open -> Maybe ( Curve Open ) )
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
It seems that GHC 9.0 is unable to use the associated type family instance TraversalCt Open clo' = clo' ~ Open
in checking that the instance signature is at least as general as the class signature. Is this expected, or an oversight?
Of course, changing the instance signature to the obviously correct
biwitherSpline
:: ( forall clo'. ( TraversalCt Open clo' )
=> Curve clo' -> Maybe ( Curve clo' )
)
-> Spline Open
-> Maybe ( Spline Open )
makes the program compile again, but I think the other instance signature should also be accepted.