#15144 closed bug (fixed)

Type inference regression between GHC 8.0.2 and 8.2.2

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.2.2
Keywords: TypeFamilies Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T15144
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (5)

comment:1 Changed 17 months ago by RyanGlScott

Keywords: TypeFamilies added

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

comment:2 Changed 17 months ago by RyanGlScott

Cc: simonpj added

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

comment:3 Changed 17 months ago by RyanGlScott

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.

comment:4 Changed 16 months ago by Simon Peyton Jones <simonpj@…>

In ae292c6d/ghc:

Do not unify representational equalities

This patch is an easy fix to Trac #15144, which was caused
by accidentally unifying a representational equality in the
unflattener.  (The main code in TcInteract was always careful
not to do so, but I'd missed the test in the unflattener.)

See Note [Do not unify representational equalities]
in TcInteract

comment:5 Changed 16 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T15144

Great report, thank you!

Note: See TracTickets for help on using tickets.