[GHC] #15144: Type inference regression between GHC 8.0.2 and 8.2.2

[GHC]

#15144: Type inference regression between GHC 8.0.2 and 8.2.2
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.2.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I observed this when debugging a test case from the `HList` library that
 works in GHC 8.0.2, but not in GHC 8.2.2 or later. Consider the following
 minimized example:

 {{{#!hs
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 import Data.Coerce
 import Data.Proxy

 type family TagR a

 class TypeIndexed r tr | r -> tr, tr -> r where
     typeIndexed ::
        (Coercible (TagR a) s, Functor f) =>
          Proxy a
       -> (tr (TagR a) -> f (tr (TagR a))) -> r s -> f (r s)

 typeIndexed' pa x = typeIndexed pa x
 }}}

 In GHC 8.0.2, the type of `typeIndexed'` is correctly inferred as:

 {{{
 $ /opt/ghc/8.0.2/bin/ghci Bug.hs
 GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Ok, modules loaded: Bug.
 λ> :t typeIndexed'
 typeIndexed'
   :: (Coercible s (TagR a), TypeIndexed r tr, Functor f) =>
      Proxy a -> (tr (TagR a) -> f (tr (TagR a))) -> r s -> f (r s)
 }}}

 In GHC 8.2.2 and later, however, the inferred type is less general:

 {{{
 $ /opt/ghc/8.4.2/bin/ghci Bug.hs
 GHCi, version 8.4.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Ok, one module loaded.
 λ> :t typeIndexed'
 typeIndexed'
   :: (TypeIndexed r tr, Functor f) =>
      Proxy a
      -> (tr (TagR a) -> f (tr (TagR a))) -> r (TagR a) -> f (r (TagR a))
 }}}

 Notice how the `Coercible s (TagR a)` constraint is no longer inferred.
 Instead, it seems that GHC is inferring the less general constraint `s ~
 TagR a`, since `s` has been substituted for `TagR a` in the type `r (TagR
 a) -> f (r (TagR a))` (whereas in 8.0.2, it was `r s -> f (r s)`).

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