GHC HEAD typechecker regression
This code, distilled from the type-level-sets
library:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
data Proxy (p :: k) = Proxy
data Set (n :: [k]) where
Empty :: Set '[]
Ext :: e -> Set s -> Set (e ': s)
type family (m :: [k]) :\ (x :: k) :: [k] where
'[] :\ x = '[]
(x ': xs) :\ x = xs
(y ': xs) :\ x = y ': (xs :\ x)
class Remove s t where
remove :: Set s -> Proxy t -> Set (s :\ t)
instance Remove '[] t where
remove Empty Proxy = Empty
instance {-# OVERLAPS #-} Remove (x ': xs) x where
remove (Ext _ xs) Proxy = xs
instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
=> Remove (y ': xs) x where
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
Typechecks in GHC 8.4.2, but not in GHC HEAD:
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:31:33: error:
• Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
bound by the instance declaration at Bug.hs:(29,31)-(30,27)
or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
bound by a pattern with constructor:
Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
in an equation for ‘remove’
at Bug.hs:31:11-18
Expected type: Set ((y : xs) :\ x)
Actual type: Set (e : (s :\ x))
• In the expression: Ext y (remove xs x)
In an equation for ‘remove’:
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
In the instance declaration for ‘Remove (y : xs) x’
• Relevant bindings include
x :: Proxy x (bound at Bug.hs:31:22)
xs :: Set s (bound at Bug.hs:31:17)
y :: e (bound at Bug.hs:31:15)
remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x)
(bound at Bug.hs:31:3)
|
31 | remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
| ^^^^^^^^^^^^^^^^^^^
This regression was introduced in commit e3dbb44f (Fix #12919 (closed) by making the flattener homegeneous.).