[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] <e_anr>_R <a_anq>_R) :: (Throws e_anr => a_anq) ~R# Wrap e_anr a_anq))) }}} Look at the lines marked `!!`. We are instantiating `(.)` with a qualified type, which is never supposed to happen. (That's essentially impredicativity.) And if you eta-expand, you get the same error with 7.10 as you do with 8.0 {{{ unthrow :: forall aa ee proxy. proxy ee -> (Throws ee => aa) -> aa unthrow _ x = unWrap (coerceWrap (Wrap x)) }}} we get {{{ * Could not deduce (Throws ee) arising from a use of `x' from the context: Throws e0 }}} So I count that as a win: 8.0 is behaving more self-consistently. Moreover, there's a good reason for it. Look at the eta-expanded version. Nothing fixes the instantiation of `e` (namely `e0`) used for `Wrap` and `unWrap` to be the same `ee` that appears in the type signature for `unthrow`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11364#comment:4> 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 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