Constructors applied to type variables behave differently starting on GHC 9.2
The following program compiles on GHC 8.6 to 9.0 but fails to compile on GHC 9.2 and HEAD. (Apologies for not reducing the test case further.)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PatternsBug where
import Data.Kind
( Type )
import Data.Proxy
( Proxy(..) )
import Data.Type.Equality
( (:~:)(Refl) )
import Unsafe.Coerce
( unsafeCoerce )
passGetterIndex
:: forall (js :: [Type]) (jss :: [[Type]]) (s :: Type) (as :: [Type])
. SSameLength js as -> HList js -> Viewers (js ': jss) s as -> Viewers jss s as
passGetterIndex (SSameSucc ( same1 :: SSameLength t_js t_as ) ) js views =
case ( js, views ) of
( (k :: j) :> (ks :: HList t_js), ConsViewer same2 (_ :: Proxy is) (_ :: Proxy iss) _ getters ) ->
case same2 of
( sameSucc@(SSameSucc (same3 :: SSameLength t_is jss) ) ) ->
case sameSucc of
( _ :: SSameLength (i ': t_is) (js ': jss) )
| Refl <- ( unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss )
, Refl <- ( unsafeCoerce Refl :: ( t_js ': MapTail jss ) :~: iss )
, Refl <- ( unsafeCoerce Refl :: i :~: j )
-- , Proxy :: Proxy bss <- Proxy @(Tail iss)
-> ConsViewer same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
( passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters )
data Viewers (iss :: [[Type]]) (s :: Type) (as :: [Type]) where
-- NilViewer ...
ConsViewer :: forall (is :: [Type]) (s :: Type) (a :: Type) (iss :: [[Type]]) (as :: [Type])
. SSameLength is (ZipCons is iss)
-> Proxy is
-> Proxy iss
-> Proxy a
-> Viewers iss s as
-> Viewers (ZipCons is iss) s (a ': as)
data SSameLength (is :: [k]) (js :: [l]) where
SSameZero :: SSameLength '[] '[]
SSameSucc :: SSameLength is js -> SSameLength (i ': is) (j ': js)
infixr 3 :>
data HList (as :: [Type]) where
HNil :: HList '[]
(:>) :: a -> HList as -> HList (a ': as)
type family ListVariadic (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
type family ZipCons (as :: [k]) (bss :: [[k]]) = (r :: [[k]]) | r -> as bss where
ZipCons '[] '[] = '[]
ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss
type family Tail (x :: [k]) :: [k] where
Tail (_ ': xs) = xs
type family MapTail (x :: [[k]]) :: [[k]] where
MapTail '[] = '[]
MapTail (xs ': xss) = Tail xs ': MapTail xssThe problem lies in the Proxy @(Tail iss) argument to the constructor ConsViewer. It causes the following error starting on GHC 9.2:
PatternsBug.hs:35:18: error:
* Could not deduce: ZipCons is2 bss ~ jss
from the context: (js ~ (i : is), as ~ (j : js1))
bound by a pattern with constructor:
SSameSucc :: forall {k} {l} (is :: [k]) (js :: [l]) (i :: k)
(j :: l).
SSameLength is js -> SSameLength (i : is) (j : js),
in an equation for `passGetterIndex'
at PatternsBug.hs:24:18-61
or from: ((js : jss) ~ ZipCons is1 iss, as ~ (a1 : as2))
bound by a pattern with constructor:
ConsViewer :: forall (is :: [*]) s a (iss :: [[*]]) (as :: [*]).
SSameLength is (ZipCons is iss)
-> Proxy is
-> Proxy iss
-> Proxy a
-> Viewers iss s as
-> Viewers (ZipCons is iss) s (a : as),
in a case alternative
at PatternsBug.hs:26:39-97
or from: (is1 ~ (i1 : is2), ZipCons is1 iss ~ (j1 : js2))
bound by a pattern with constructor:
SSameSucc :: forall {k} {l} (is :: [k]) (js :: [l]) (i :: k)
(j :: l).
SSameLength is js -> SSameLength (i : is) (j : js),
in a case alternative
at PatternsBug.hs:28:21-61
or from: jss ~ ZipCons is2 (Tail iss)
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
a case alternative
at PatternsBug.hs:31:17-20
or from: iss ~ (is : MapTail jss)
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
a case alternative
at PatternsBug.hs:32:17-20
Expected: Viewers jss s as
Actual: Viewers (ZipCons is2 bss) s (j : js1)
`jss' is a rigid type variable bound by
the type signature for:
passGetterIndex :: forall (js :: [*]) (jss :: [[*]]) s (as :: [*]).
SSameLength js as
-> HList js -> Viewers (js : jss) s as -> Viewers jss s as
at PatternsBug.hs:(21,1)-(23,81)
* In the expression:
ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
In a case alternative:
(_ :: SSameLength (i : t_is) (js : jss))
| Refl <- (unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss),
Refl <- (unsafeCoerce Refl :: (t_js : MapTail jss) :~: iss),
Refl <- (unsafeCoerce Refl :: i :~: j)
-> ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
In the expression:
case sameSucc of
(_ :: SSameLength (i : t_is) (js : jss))
| Refl <- (unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss),
Refl <- (unsafeCoerce Refl :: (t_js : MapTail jss) :~: iss),
Refl <- (unsafeCoerce Refl :: i :~: j)
-> ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
* Relevant bindings include
same3 :: SSameLength is2 jss (bound at PatternsBug.hs:28:32)
views :: Viewers (js : jss) s as (bound at PatternsBug.hs:24:68)
passGetterIndex :: SSameLength js as
-> HList js -> Viewers (js : jss) s as -> Viewers jss s as
(bound at PatternsBug.hs:24:1)
|
35 | -> ConsViewer same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
PatternsBug.hs:35:50: error:
* Couldn't match type `bss' with `MapTail jss'
Expected: Proxy bss
Actual: Proxy (Tail iss)
`bss' is untouchable
inside the constraints: a ~ i1
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
a case alternative
at PatternsBug.hs:33:17-20
* In the third argument of `ConsViewer', namely
`(Proxy @(Tail iss))'
In the expression:
ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
In a case alternative:
(_ :: SSameLength (i : t_is) (js : jss))
| Refl <- (unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss),
Refl <- (unsafeCoerce Refl :: (t_js : MapTail jss) :~: iss),
Refl <- (unsafeCoerce Refl :: i :~: j)
-> ConsViewer
same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
(passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters)
* Relevant bindings include
same3 :: SSameLength is2 jss (bound at PatternsBug.hs:28:32)
views :: Viewers (js : jss) s as (bound at PatternsBug.hs:24:68)
passGetterIndex :: SSameLength js as
-> HList js -> Viewers (js : jss) s as -> Viewers jss s as
(bound at PatternsBug.hs:24:1)
|
35 | -> ConsViewer same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
| ^^^^^^^^^^^^^^^^^Rather curiously, if you uncomment the line
Proxy :: Proxy bss <- Proxy @(Tail iss)and use bss instead of Tail iss just below, writing:
-> ConsViewer same3 (Proxy @t_is) (Proxy @bss) Proxy
( passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters )then all of a sudden GHC 9.2 accepts this program again. So it seems like there is a special treament for type variables compared to other types. This perhaps makes when the constructor is used as a pattern, but it's rather strange that it would make any difference when it's an expression.