[GHC] #14618: Higher rank typechecking is broken
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The oddity was noticed when someone asked the type of `lens` from lambdabot and it replied with {{{#!hs 1514165211 [04:26:51] <lambdabot> Functor f => (s1 -> a1) -> (s1 -> b1 -> t1) -> (a2 -> f b2) -> s2 -> f t2 }}} This disagrees with `lens`'s type per definition (way too many foralls and unconstrained type variables), and if handled carefully it could be used to implement `unsafeCoerce` within SafeHaskell. The minimalest example I could come up with: {{{#!hs {-# LANGUAGE RankNTypes #-} safeCoerce :: a -> b safeCoerce = f' where f :: d -> forall c. d f x = x f' = f }}} This compiles and typechecks on GHC 8.2.2, 8.2.1 (courtesy of hydraz) and HEAD. But not on 8.0.2 (hydraz) or 7.10.3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by int-e): * cc: int-e (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): There is a core lint error at least.. {{{ [1 of 1] Compiling Foo ( unco.hs, unco.o ) *** Core Lint errors : in result of Desugar (after optimization) *** unco.hs:5:1: warning: [RHS of safeCoerce :: forall a b. a -> b] The type of this binder doesn't match the type of its RHS: safeCoerce Binder's type: forall a b. a -> b Rhs type: forall a b. b -> b *** Offending Program *** safeCoerce :: forall a b. a -> b [LclIdX] safeCoerce = \ (@ a_ao7) (@ b_ao8) -> let { f_anO :: forall d. d -> forall c. d [LclId] f_anO = \ (@ d_aop) (dk_aSV :: d_aop) (@ c_aos) -> dk_aSV } in \ (di_aSY :: b_ao8) -> f_anO @ b_ao8 di_aSY @ Any $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Foo"#) *** End of Offense *** <no location info>: error: Compilation had errors }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): How utterly frightening. I have a fix. Validating now. Thanks for the wonderfully simple test case! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mniip): Can't help but be curious about what caused this. Something related to broken instantiation before constraint solving, or overzealous generalization afterwards? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken
-------------------------------------+-------------------------------------
Reporter: mniip | Owner: (none)
Type: bug | Status: new
Priority: highest | Milestone:
Component: Compiler (Type | Version: 8.2.2
checker) |
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC accepts | Unknown/Multiple
invalid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: merge Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC accepts | Test Case: invalid program | typecheck/should_fail/T14618 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => typecheck/should_fail/T14618 * milestone: => 8.4.1 Comment: You can see the commit. It was just a simple oversight in propagating an instantiating substitution. This should certainly be merged. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: merge Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC accepts | Test Case: invalid program | typecheck/should_fail/T14618 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mniip): Should this be backported to 8.2? I feel like a complete violation of SafeHaskell might be a fairly serious concern to some users. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: merge Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC accepts | Test Case: invalid program | typecheck/should_fail/T14618 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, I think so. To be honest, I wasn't sure how to set the Milestone tag to make sure it gets into both 8.2.3 and 8.4.1. But Safe Haskell isn't safe anyway: see #9562. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: merge Priority: highest | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC accepts | Test Case: invalid program | typecheck/should_fail/T14618 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.4.1 => 8.2.3 Comment: Merged to ghc-8.4 with 1779e3bf4876d8ac46657275e5f0f2ee6877a5c9. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14618: Higher rank typechecking is broken -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: merge Priority: highest | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC accepts | Test Case: invalid program | typecheck/should_fail/T14618 Blocked By: 14620 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * blockedby: => 14620 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14618#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC