#14323: Occurs check regressions in GHC 8.2.1 (and HEAD) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (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: -------------------------------------+------------------------------------- Inspired by adamse's comment at https://ghc.haskell.org/trac/ghc/ticket/14317#comment:3, I've discovered some programs which behave differently on GHC 8.0.2, 8.2.1, and HEAD. ----- First, there's this program: {{{#!hs {-# 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: {{{#!hs {-# 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: {{{#!hs {-# 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 | ^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14323 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler