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

4 May 2018

      #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@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
 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