GitLab

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.).