[GHC] #11364: Possible type-checker regression in GHC 8.0
#11364: Possible type-checker regression in GHC 8.0 -------------------------------------+------------------------------------- Reporter: hvr | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 (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: -------------------------------------+------------------------------------- The following code fragment works with GHCs prior to GHC 8.0 but not with GHC 8.0: {{{#!hs {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE IncoherentInstances #-} {-# LANGUAGE RankNTypes #-} module Issue where import Data.Coerce (coerce) data Proxy a = Proxy newtype Catch a = Catch a class Throws e type role Throws representational instance Throws (Catch e) newtype Wrap e a = Wrap { unWrap :: Throws e => a } coerceWrap :: Wrap e a -> Wrap (Catch e) a coerceWrap = coerce unthrow :: proxy e -> (Throws e => a) -> a unthrow _ = unWrap . coerceWrap . Wrap {- this works in GHC 7.10.3, but fails in GHC 8.0 with GHCi, version 8.0.0.20160105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Issue ( Issue.hs, interpreted ) Issue.hs:25:13: error: • Could not deduce (Throws e) from the context: Throws e0 bound by a type expected by the context: Throws e0 => a at Issue.hs:26:13-38 Possible fix: add (Throws e) to the context of the type signature for: unthrow :: proxy e -> (Throws e => a) -> a • In the expression: unWrap . coerceWrap . Wrap In an equation for ‘unthrow’: unthrow _ = unWrap . coerceWrap . Wrap Failed, modules loaded: none. -} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11364 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11364: Possible type-checker regression in GHC 8.0 -------------------------------------+------------------------------------- Reporter: hvr | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by hvr): Changing the type-signature to {{{#!hs unthrow :: Throws e => proxy e -> (Throws e => a) -> a }}} In fact makes the code compile... but is this a regression or not? :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11364#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11364: Possible type-checker regression in GHC 8.0 -------------------------------------+------------------------------------- Reporter: hvr | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by hvr): Here's a blog post motivating this code (thanks Ben!): http://www.well-typed.com/blog/2015/07/checked-exceptions/ -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11364#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11364: Possible type-checker regression in GHC 8.0 -------------------------------------+------------------------------------- Reporter: hvr | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): It may make it compile, but it breaks the intended semantics of `unthrow`. I would expect that this is a regression. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11364#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11364: Possible type-checker regression in GHC 8.0
-------------------------------------+-------------------------------------
Reporter: hvr | Owner:
Type: bug | Status: closed
Priority: highest | Milestone: 8.0.1
Component: Compiler (Type | Version: 7.10.3
checker) |
Resolution: invalid | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Changes (by simonpj):
* status: new => closed
* resolution: => invalid
Comment:
I think that 7.10 is wrong. It generates this elaborated program
{{{
unthrow =
\ (@ a_anq) (@ e_anr) (@ (proxy_ans :: * -> *)) _ [Occ=Dead] ->
. @ (Wrap (Catch e_anr) a_anq)
@ a_anq
!! @ (Throws e_anr => a_anq)
(unWrap @ (Catch e_anr) @ a_anq (T11364.$fThrowsCatch @ e_anr))
(. @ (Wrap e_anr a_anq)
@ (Wrap (Catch e_anr) a_anq)
!! @ (Throws e_anr => a_anq)
(coerceWrap @ e_anr @ a_anq)
(\ (tpl_B1 :: Throws e_anr => a_anq) ->
tpl_B1
`cast` (Sym (T11364.NTCo:Wrap[0]
#11364: Possible type-checker regression in GHC 8.0 -------------------------------------+------------------------------------- Reporter: hvr | Owner: Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): You can make it compile by adding a signature to fix `e0` to be `ee`. For example: {{{ unthrow :: forall aa ee proxy. proxy ee -> (Throws ee => aa) -> aa unthrow _ x = unWrap (coerceWrap (Wrap x :: Wrap ee aa)) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11364#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11364: Possible type-checker regression in GHC 8.0 -------------------------------------+------------------------------------- Reporter: hvr | Owner: Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by edsko): * cc: edsko (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11364#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11364: Possible type-checker regression in GHC 8.0 -------------------------------------+------------------------------------- Reporter: hvr | Owner: Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): So should this ticket be closed? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11364#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC