Type inference regression between GHC 8.0.2 and 8.2.2

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:

{-# 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)).

Trac metadata

Trac field	Value
Version	8.2.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import typechecker labels

Here's a slightly smaller test case:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Coerce
import Data.Proxy

type family F x

f :: Coercible (F a) b => Proxy a -> F a -> b
f _ = coerce

g p x = f p x

$ /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 g
g :: Coercible b (F a) => Proxy a -> F a -> b

$ /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 g
g :: Proxy a -> F a -> F a

This regression was introduced in commit 1eec1f21 (Another major constraint-solver refactoring).

What's odd is that things work out alright if I write an explicit type signature:

g :: Coercible (F a) b => Proxy a -> F a -> b
g p x = f p x

It's only when the type is inferred that it becomes less general.

mentioned in commit ae292c6d

closed

Great report, thank you!

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → indexed-types/should_compile/T15144

added Pnormal label