[GHC] #12531: Holes should be kind-polymorphic
#12531: Holes should be kind-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Other Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I often use holes while writing long expressions out in GHCi in order to let the typechecker assist me with type inference. Sometimes though I find myself in a situation where I want to use holes near unlifted types and results in kind check messages obscuring the holes or having hole errors not show up at all: {{{#!hs
I# (_ +# 1#)
<interactive>:5:5: error: • Couldn't match a lifted type with an unlifted type When matching the kind of ‘Int#’ • In the first argument of ‘(+#)’, namely ‘_’ In the first argument of ‘I#’, namely ‘(_ +# 1#)’ In the expression: I# (_ +# 1#) <interactive>:5:5: error: • Found hole: _ :: Int# • In the first argument of ‘(+#)’, namely ‘_’ In the first argument of ‘I#’, namely ‘(_ +# 1#)’ In the expression: I# (_ +# 1#) • Relevant bindings include it :: Int (bound at <interactive>:5:1) }}} (Don't be deceived, the type of `_` there is actually `Int# |> (TYPE U(hole:{a1qG}, 'IntRep, 'PtrRepLifted)_N)_N`) Perhaps the type of `_` should be `forall r (a :: TYPE r). a` or even `forall k (a :: k). a` instead? This might lead to issues with `-fdefer-typed-holes` but maybe we could at first disallow deferred unlifted-kinded holes? But in theory a hole is just a call to `error` which is representation-polymorphic already. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be kind-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by mniip: @@ -5,2 +5,2 @@ - near unlifted types and results in kind check messages obscuring the holes - or having hole errors not show up at all: + near unlifted types and that results in kind check messages obscuring the + holes or having hole errors not show up at all: New description: I often use holes while writing long expressions out in GHCi in order to let the typechecker assist me with type inference. Sometimes though I find myself in a situation where I want to use holes near unlifted types and that results in kind check messages obscuring the holes or having hole errors not show up at all: {{{#!hs
I# (_ +# 1#)
<interactive>:5:5: error: • Couldn't match a lifted type with an unlifted type When matching the kind of ‘Int#’ • In the first argument of ‘(+#)’, namely ‘_’ In the first argument of ‘I#’, namely ‘(_ +# 1#)’ In the expression: I# (_ +# 1#) <interactive>:5:5: error: • Found hole: _ :: Int# • In the first argument of ‘(+#)’, namely ‘_’ In the first argument of ‘I#’, namely ‘(_ +# 1#)’ In the expression: I# (_ +# 1#) • Relevant bindings include it :: Int (bound at <interactive>:5:1) }}} (Don't be deceived, the type of `_` there is actually `Int# |> (TYPE U(hole:{a1qG}, 'IntRep, 'PtrRepLifted)_N)_N`) Perhaps the type of `_` should be `forall r (a :: TYPE r). a` or even `forall k (a :: k). a` instead? This might lead to issues with `-fdefer-typed-holes` but maybe we could at first disallow deferred unlifted-kinded holes? But in theory a hole is just a call to `error` which is representation-polymorphic already. -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be representation-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This looks quite plausible and shouldn't be hard to implement. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be representation-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"ae66f356fb0dbf79dab1074d71275904c448b329/ghc" ae66f35/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="ae66f356fb0dbf79dab1074d71275904c448b329" Allow typed holes to be levity-polymorphic This one-line change fixes Trac #12531. Hooray. Simple, non-invasive; can merge to 8.0.2 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be representation-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"0050aff22ba04baca732bf5124002417ab667f8a/ghc" 0050aff2/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="0050aff22ba04baca732bf5124002417ab667f8a" Fix scoping of type variables in instances This fixes Trac #12531: class Foo x where foo :: forall a . x a -> x a default foo :: forall b . x b -> x b foo x = go where go :: x b go = undefined We want 'b' to scope over the code for 'foo', but we were using 'a' instead. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be representation-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: merge Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: partial- | sigs/should_compile/T12531 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => partial-sigs/should_compile/T12531 Comment: We could merge this too I think. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be representation-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: merge Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: partial- | sigs/should_compile/T12531 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Indeed, I'm fine with merging this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be representation-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: merge Priority: normal | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: partial- | sigs/should_compile/T12531 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * milestone: => 8.0.2 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12531: Holes should be representation-polymorphic -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: feature request | Status: closed Priority: normal | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: partial- | sigs/should_compile/T12531 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.0` as f4ac734d754e2d4399525038e8a4dd4a841ce8af. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12531#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC