[GHC] #15122: GHC HEAD typechecker regression involving overlapping instances (was: Compiling a library problem with a local 8.5 build)

[GHC]

#15122: GHC HEAD typechecker regression involving overlapping instances
-------------------------------------+-------------------------------------
        Reporter:  fmixing           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * priority:  normal => highest
 * os:  MacOS X => Unknown/Multiple
 * component:  Compiler => Compiler (Type checker)
 * architecture:  x86_64 (amd64) => Unknown/Multiple


Comment:

 Here is a slightly more minimal example:

 {{{#!hs
 {-# 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 at Proxy) = Ext y (remove xs x)
 }}}

 In GHC 8.4.2, this typechecks, but in GHC HEAD, it fails with:

 {{{
 $ /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 at 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 at Proxy) = Ext y (remove xs x)
    |                                 ^^^^^^^^^^^^^^^^^^^
 }}}

 I'm unclear on what the exact culprit is here, so feel free to change the
 title further if overlapping instances turn out not to be the problem.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15122#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler