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

[GHC]

#15122: GHC HEAD typechecker regression
-------------------------------------+-------------------------------------
        Reporter:  fmixing           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
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):

 * keywords:   => TypeInType


Comment:

 Never mind, I don't think this has anything to do with overlapping
 instances (or even type classes in particular), since the following also
 typechecks on GHC 8.4 but not on HEAD:

 {{{#!hs
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

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

 remove :: forall x y xs.
           ((y : xs) :\ x) ~ (y : (xs :\ x))
        => Set (y ': xs) -> Proxy x -> Set ((y ': xs) :\ x)
 remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs))

 remove' :: Set s -> Proxy x -> Proxy xs -> Set (xs :\ x)
 remove' = undefined
 }}}

 Here's the error message on HEAD if you compile with `-fprint-explicit-
 kinds`:

 {{{
 $ /opt/ghc/head/bin/ghc -fprint-explicit-kinds Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:24:23: error:
     • Could not deduce: ((:\) * ((':) * e s) x :: [*])
                         ~~ ((':) * e ((:\) * s x) :: [*])
       from the context: (:\) k ((':) k y xs) x ~ (':) k y ((:\) k xs x)
         bound by the type signature for:
                    remove :: forall k (x :: k) (y :: k) (xs :: [k]).
                              ((:\) k ((':) k y xs) x ~ (':) k y ((:\) k xs
 x)) =>
                              Set k ((':) k y xs) -> Proxy k x -> Set k
 ((:\) k ((':) k y xs) x)
         at Bug.hs:(21,1)-(23,58)
       or from: ((k :: *) ~~ (* :: *),
                 ((':) 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:24:9-16
       Expected type: Set k ((:\) k ((':) k y xs) x)
         Actual type: Set * ((':) * e ((:\) * s x))
     • In the expression: Ext y (remove' xs x (Proxy :: Proxy xs))
       In an equation for ‘remove’:
           remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs))
     • Relevant bindings include
         x :: Proxy k x (bound at Bug.hs:24:19)
         xs :: Set * s (bound at Bug.hs:24:15)
         y :: e (bound at Bug.hs:24:13)
         remove :: Set k ((':) k y xs)
                   -> Proxy k x -> Set k ((:\) k ((':) k y xs) x)
           (bound at Bug.hs:24:1)
    |
 24 | remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs))
    |                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

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