Constraint solver regression in 9.2
Summary
While trying to make the generics-sop
and sop-core
packages compatible with GHC 9.2, I discovered a regression in the constraint solver. The included program compiles at with GHC 9.0.1, GHC 8.8.4, GHC 8.6.5, GHC 8.4.4, GHC 8.2.2, but it fails with GHC 9.2 with the following error message:
AllEq.hs:19:21: error:
• Couldn't match type ‘ys0’ with ‘Head ys0 : Tail ys0’
arising from a use of ‘convert’
• In the second argument of ‘const’, namely ‘(convert xs)’
In the expression: const () (convert xs)
In an equation for ‘test’: test xs = const () (convert xs)
|
19 | test xs = const () (convert xs)
| ^^^^^^^
Steps to reproduce
Run ghc
or ghci
on the following file:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module AllEq where
import Data.Kind
import Data.Proxy
convert :: (AllEq xs ys) => Proxy xs -> Proxy ys
convert p = Proxy
-- Works with ghc up to 9.0. Fails with ghc 9.2.
test :: Proxy '[Char, Bool] -> ()
test xs = const () (convert xs)
class (AllEqF xs ys, SameShapeAs xs ys) => AllEq (xs :: [a]) (ys :: [a])
instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
type family SameShapeAs (xs :: [a]) (ys :: [a]) :: Constraint where
SameShapeAs '[] ys = (ys ~ '[])
SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))
type family AllEqF (xs :: [a]) (ys :: [a]) :: Constraint where
AllEqF '[] '[] = ()
AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)
type family Head (xs :: [a]) :: a where
Head (x : xs) = x
type family Tail (xs :: [a]) :: [a] where
Tail (x : xs) = xs
Expected behavior
I would expect the program to be accepted.
Environment
- GHC version used: 9.2.0.20210406, built locally on my machine from the
ghc-9.2
branch at commit d197fb3d
Optional:
- Operating System: Linux (NixOS)
- System Architecture: x86_64