[GHC] #15122: GHC HEAD typechecker regression involving overlapping instances

[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:                    |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:

Old description:

> I’ve discovered that one library throws type checking exception when I
> try to compile it with my version of ghc compiler (I build it using
> `cabal new-build --with-compiler=/usr/local/bin/ghc-8.5.20180504`, the
> compiler was built from the master with
> 56974323ed427988059b5153bb43c694358cbb9b as the last commit), but it
> builds with 8.4.2 compiler (`cabal new-build --with-
> compiler=/usr/local/bin/ghc-8.4.2`). It’s really strange, so I tried to
> `make` the local version of 8.4.2 in the branch ghc-8.4.2-release, and
> found out that it cannot be built because there are missing some files
> that are necessary for build.  So maybe I’m doing something wrong? And
> can it be that this library doesn’t type check with 8.5 because it’s
> built from source files?
>
> The exception can be seen here:
> https://gist.github.com/fmixing/93d140dc7dbe25199af28616c6a143da

New description:

 This code, distilled from the `type-level-sets` library:

 {{{#!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)
 }}}

 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 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)
    |                                 ^^^^^^^^^^^^^^^^^^^
 }}}

 This regression was introduced in commit
 e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the
 flattener homegeneous.).

--

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