[GHC] #13778: explicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression position
#13778: explicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression position -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Keywords: | Operating System: Unknown/Multiple PatternSynonyms | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Compile this {{{#!hs pattern One <- ((==One) -> True) where One = 1 }}} I get {{{ test.hs:1:1: error: Recursive pattern synonym definition with following bindings: One (defined at test.hs:(1,1)-(1,15)) | Compilation failed. }}} Note that the error is due to the usage in view pattern **expression position**. But for ''explicitly bidirectional'' patterns, there is no recursivity going on. So this usage should be allowed. I am testing with HEAD, but the issue is probably older. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13778> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13778: explicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression position -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms 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 Iceland_jack): * cc: Iceland_jack (added) Comment: This would be good to have -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13778#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13778: explicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression position -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms 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): Harump. I think you want 1. To infer the type of `One` from its "builder" {{{ One = 1 }}} 2. To use that type when inferring the type of the pattern But actually GHC does it the other way round 1. Infer the type of the pattern 2. Use that in checking the type of the "builder" There's a good reason for this. Here's a Note from `RnBinds`: {{{ Note [Pattern synonym builders don't yield dependencies] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When renaming a pattern synonym that has an explicit builder, references in the builder definition should not be used when calculating dependencies. For example, consider the following pattern synonym definition: pattern P x <- C1 x where P x = f (C1 x) f (P x) = C2 x In this case, 'P' needs to be typechecked in two passes: 1. Typecheck the pattern definition of 'P', which fully determines the type of 'P'. This step doesn't require knowing anything about 'f', since the builder definition is not looked at. 2. Typecheck the builder definition, which needs the typechecked definition of 'f' to be in scope; done by calls oo tcPatSynBuilderBind in TcBinds.tcValBinds. This behaviour is implemented in 'tcValBinds', but it crucially depends on 'P' not being put in a recursive group with 'f' (which would make it look like a recursive pattern synonym a la 'pattern P = P' which is unsound and rejected). }}} So I don't see an easy way to give you want you want. The only think I can think of is to allow some kind of monomorphic recursion. But it's easy to program around, so I'm disinclined to fiddle. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13778#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13778: explicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression position -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms 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 heisenbug): Replying to [comment:2 simonpj]: Hi Simon, adding a type signature won't make the error go away. IIRC this is not a type inference problem. I cannot try now, am AFK.
Harump. I think you want
1. To infer the type of `One` from its "builder" {{{ One = 1 }}}
2. To use that type when inferring the type of the pattern
But actually GHC does it the other way round
1. Infer the type of the pattern 2. Use that in checking the type of the "builder"
There's a good reason for this. Here's a Note from `RnBinds`: {{{ Note [Pattern synonym builders don't yield dependencies] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When renaming a pattern synonym that has an explicit builder, references in the builder definition should not be used when calculating dependencies. For example, consider the following pattern synonym definition:
pattern P x <- C1 x where P x = f (C1 x)
f (P x) = C2 x
In this case, 'P' needs to be typechecked in two passes:
1. Typecheck the pattern definition of 'P', which fully determines the type of 'P'. This step doesn't require knowing anything about 'f', since the builder definition is not looked at.
2. Typecheck the builder definition, which needs the typechecked definition of 'f' to be in scope; done by calls oo tcPatSynBuilderBind in TcBinds.tcValBinds.
This behaviour is implemented in 'tcValBinds', but it crucially depends on 'P' not being put in a recursive group with 'f' (which would make it look like a recursive pattern synonym a la 'pattern P = P' which is unsound and rejected). }}} So I don't see an easy way to give you want you want.
The only think I can think of is to allow some kind of monomorphic recursion. But it's easy to program around, so I'm disinclined to fiddle.
-- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13778#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13778: explicitly bidirectional patterns should not report Recursive definition" when used in view pattern expression position -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms 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):
adding a type signature won't make the error go away
I didn't claim that it would! But you give me an idea. If you wrote a pattern signature: {{{ pattern One :: Num a => a pattern One <- ((==One) -> True) where One = 1 }}} then I think we could soundly suppress the check, without messing up the architecture above. Hmm. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13778#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC