[GHC] #11186: Give strong preference to type variable names in scope when reporting hole contexts
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: typed-holes | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like {{{#!hs foo :: forall bar . ... foo = ... _ ... }}} and yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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): Can you give a concrete example? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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 dfeuer): Replying to [comment:1 simonpj]:
Can you give a concrete example?
I finally found one, attempting to figure out how to write something like `reverse` for type-aligned lists. In this case, I use a pattern signature to name an existentially quantified type, but GHC's message doesn't seem to respect that. {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module TAList where import Control.Category import Prelude hiding ((.), id) data TAList (cat :: k -> k -> *) (x :: k) (z :: k) where Nil :: TAList cat x x (:<) :: cat b c -> TAList cat a b -> TAList cat a c infixr 5 :< newtype Op cat x y = Op {op :: cat y x} reverseOntoTA :: TAList cat b d -> TAList (Op cat) d a -> TAList (Op cat) d a reverseOntoTA Nil ys = ys reverseOntoTA ((x :: cat c d) :< (xs :: TAList cat b c)) ys = _ }}} I named the unknown type variable `c`, but GHC says: {{{ Relevant bindings include ys :: TAList (Op cat) d a (bound at TAList.hs:32:58) xs :: TAList cat b b1 (bound at TAList.hs:32:35) x :: cat b1 d (bound at TAList.hs:32:17) reverseOntoTA :: TAList cat b d -> TAList (Op cat) d a -> TAList (Op cat) d a }}} That is, it's decided to name that variable `b1` instead. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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 dfeuer): It looks like it may be preferring the name of the type variable used in the GADT definition to the one in the pattern, which seems very wrong to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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 dfeuer): Now that I know what to look for, I found a much smaller example: {{{#!hs {-# LANGUAGE ExistentialTypes #-} {-# LANGUAGE ScopedTypeVariables #-} data Foop = forall xx . Foop xx blah (Foop (q :: pah)) = _ }}} Here GHC again ignores the requested `pah` variable in favor of `xx`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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): OK I understand. Here is a version of comment:4 that actually shows the problem {{{ {-# LANGUAGE ExistentialQuantification, ScopedTypeVariables #-} module T11186 where data Foop = forall xx . Foop xx blah (Foop (q :: pah)) = length ([q] :: _) }}} We get {{{ T11186.hs:8:41: error: • Found type wildcard ‘_’ standing for ‘[xx]’ Where: ‘xx’ is a rigid type variable bound by a pattern with constructor: Foop :: forall xx. xx -> Foop, in an equation for ‘blah’ at T11186.hs:8:7 }}} Now, the difficulty is this: lexically scoped type variable might be bound somewhere very different to the existential pattern itself. For example: {{{ bla2 (Foop q) = (\(r::pah) -> length ([r] :: _)) q }}} And indeed, the same skolem bound in the pattern might have different lexical names in different places: {{{ bla2 (Foop q) = ( (\(r::pah) -> length ([r] :: _)) q , (\(r::hap) -> length ([r] :: _)) q ) }}} Now what would you expect? Ugh. Tiresome, and not particularly easy to fix. * Visible type application will let you bind the type variable in the pattern (which is where it "ought" to be bound * Maybe some hack could do a better job when the type variable is in fact bound in the pattern where the existential is born. Funnily enough, Richard, Stephanie, Adam, and I were discussing questions around lexically scoped type variables only last week. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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): * cc: goldfire, sweirich, adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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 dfeuer): Replying to [comment:5 simonpj]:
And indeed, the same skolem bound in the pattern might have different lexical names in different places: {{{ bla2 (Foop q) = ( (\(r::pah) -> length ([r] :: _x)) q , (\(r::hap) -> length ([r] :: _y)) q ) }}} Now what would you expect?
I would expect the report about `_x` to tell me about `pah` and the one about `_y` to tell me about `hap`. May I ask what you think will be hard about this? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: typed-holes 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):
May I ask what you think will be hard about this?
Well, the message prints the type of `[r]`, and the type is the ''same in both cases''. Your point, which is a reasonable one, is that you'd like the type to be rewritten to make sense in the current lexical context, whatever that is. I don't think that would be too hard. The current lexical environment maps, say `pah :-> t8`, where `t8` is the variable GHC chose for the argument type of `q`. So we could reverse-map back from `t8` to `pah`. Not hard, but more than the work of a moment. I can advise if someone wants to have a go. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: TypedHoles 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): * keywords: typed-holes => TypedHoles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11186#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC