Constraint solver regression in 9.2
Summary
When porting some generics-sop code from GHC 8.10 to GHC 9.2, I discovered a regression in the type checker.
Steps to reproduce
Run GHC on the following program:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module ConstraintTest2 where
import Data.Kind
type family Code a :: [[Type]]
type IsWrappedType a x = Code a ~ '[ '[ x ] ]
type IsProductType a xs = Code a ~ '[ xs ]
type family Head (xs :: [a]) :: a where
Head (x : xs) = x
type ProductCode a = Head (Code a)
type WrappedCode a = Head (Head (Code a))
wrappedTypeTo :: IsWrappedType a x => x -> a
wrappedTypeTo = undefined
to :: SOP (Code a) -> a
to = undefined
data SOP (xss :: [[a]])
type WrappedProduct a = (IsWrappedType a (WrappedCode a), IsProductType (WrappedCode a) (ProductCode (WrappedCode a)))
process :: (SOP '[ xs ] -> a) -> a
process = undefined
-- works with 8.10 and 9.0, fails with 9.2
test :: WrappedProduct a => a
test = process (wrappedTypeTo . to)
Expected behavior
I expect the program to compile, as it does with GHC 8.10 and GHC 9.0. However, with GHC 9.2, I get:
/home/andres/trans/ConstraintTest2.hs:37:17: error:
• Could not deduce: Code a ~ '[ '[b0]]
arising from a use of ‘wrappedTypeTo’
from the context: WrappedProduct a
bound by the type signature for:
test :: forall a. WrappedProduct a => a
at /home/andres/trans/ConstraintTest2.hs:36:1-29
The type variable ‘b0’ is ambiguous
• In the first argument of ‘(.)’, namely ‘wrappedTypeTo’
In the first argument of ‘process’, namely ‘(wrappedTypeTo . to)’
In the expression: process (wrappedTypeTo . to)
• Relevant bindings include
test :: a (bound at /home/andres/trans/ConstraintTest2.hs:37:1)
|
37 | test = process (wrappedTypeTo . to)
| ^^^^^^^^^^^^^
/home/andres/trans/ConstraintTest2.hs:37:33: error:
• Could not deduce: Code b0 ~ '[xs0]
from the context: WrappedProduct a
bound by the type signature for:
test :: forall a. WrappedProduct a => a
at /home/andres/trans/ConstraintTest2.hs:36:1-29
Expected: SOP '[xs0] -> b0
Actual: SOP (Code b0) -> b0
The type variables ‘b0’, ‘xs0’ are ambiguous
• In the second argument of ‘(.)’, namely ‘to’
In the first argument of ‘process’, namely ‘(wrappedTypeTo . to)’
In the expression: process (wrappedTypeTo . to)
|
37 | test = process (wrappedTypeTo . to)
| ^^
Environment
- GHC version used: 9.2.2