Occurs check regressions in GHC 8.2.1 (and HEAD)

Inspired by adamse's comment at #14317##14323 (closed), I've discovered some programs which behave differently on GHC 8.0.2, 8.2.1, and HEAD.

---

First, there's this program:

{-# LANGUAGE GADTs #-}

hm1 :: b ~ f b => b -> f b
hm1 x = x

On GHC 8.0.2, this compiles (with a warning):

GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:4:1: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In an equation for ‘hm1’: hm1 x = ...

But on GHC 8.2.1, it errors:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:4:9: error:
    • Could not deduce: b ~ f b
      from the context: b ~ f b
        bound by the type signature for:
                   hm1 :: forall b (f :: * -> *). b ~ f b => b -> f b
        at Bug.hs:3:1-26
      ‘b’ is a rigid type variable bound by
        the type signature for:
          hm1 :: forall b (f :: * -> *). b ~ f b => b -> f b
        at Bug.hs:3:1-26
    • In the expression: x
      In an equation for ‘hm1’: hm1 x = x
    • Relevant bindings include
        x :: b (bound at Bug.hs:4:5)
        hm1 :: b -> f b (bound at Bug.hs:4:1)
  |
4 | hm1 x = x
  |         ^

And on GHC HEAD, it fails with a different error!

GHCi, version 8.3.20171004: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:4:9: error:
    • Occurs check: cannot construct the infinite type: b ~ f b
    • In the expression: x
      In an equation for ‘hm1’: hm1 x = x
    • Relevant bindings include
        x :: b (bound at Bug.hs:4:5)
        hm1 :: b -> f b (bound at Bug.hs:4:1)
  |
4 | hm1 x = x
  |         ^

The same errors occur if you give hm1 the type hm1 :: b ~ f b => f b -> b.

---

What happens if you try Coercible instead of (~)? Consider this variant of the program above:

{-# LANGUAGE GADTs #-}

import Data.Coerce

hm2 :: Coercible b (f b) => b -> f b
hm2 = coerce

On GHC 8.0.2, 8.2.1, and HEAD, this compiles (without warnings). Good. But if you change the type to use the symmetric version of that constraint:

{-# LANGUAGE GADTs #-}

import Data.Coerce

hm3 :: Coercible (f b) b => b -> f b
hm3 = coerce

Then on GHC 8.0.2, it compiles without warnings, but on 8.2.1 and HEAD it fails!

Here is the error with 8.2.1:

Bug3.hs:6:7: error:
    • Could not deduce: Coercible b (f b)
        arising from a use of ‘coerce’
      from the context: Coercible (f b) b
        bound by the type signature for:
                   hm3 :: forall (f :: * -> *) b. Coercible (f b) b => b -> f b
        at Bug3.hs:5:1-36
      ‘b’ is a rigid type variable bound by
        the type signature for:
          hm3 :: forall (f :: * -> *) b. Coercible (f b) b => b -> f b
        at Bug3.hs:5:1-36
    • In the expression: coerce
      In an equation for ‘hm3’: hm3 = coerce
    • Relevant bindings include hm3 :: b -> f b (bound at Bug3.hs:6:1)
  |
6 | hm3 = coerce
  |       ^^^^^^

And on HEAD:

Bug3.hs:6:7: error:
    • Occurs check: cannot construct the infinite type: b ~ f b
        arising from a use of ‘coerce’
    • In the expression: coerce
      In an equation for ‘hm3’: hm3 = coerce
    • Relevant bindings include hm3 :: b -> f b (bound at Bug3.hs:6:1)
  |
6 | hm3 = coerce
  |       ^^^^^^

Trac metadata

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