[GHC] #15685: Pattern signature not inferred
#15685: Pattern signature not inferred -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 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: -------------------------------------+------------------------------------- Should this pattern synonym declaration fail, {{{#!hs {-# Language DataKinds, TypeOperators, PolyKinds, GADTs, PatternSynonyms #-} import Data.Kind data NS f as where Here :: f a -> NS f (a:as) data NP :: (k -> Type) -> ([k] -> Type) where Nil :: NP f '[] pattern HereNil = Here Nil }}} {{{ $ ghci -ignore-dot-ghci hs/457.hs GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( hs/457.hs, interpreted ) [flags changed] hs/457.hs:11:19: error: • Could not deduce: f ~~ NP f0 from the context: (as ~ (a1 : as1), GHC.Types.Any ~ '[]) bound by the signature for pattern synonym ‘HereNil’ at hs/457.hs:11:1-26 ‘f’ is a rigid type variable bound by the signature for pattern synonym ‘HereNil’ at hs/457.hs:11:1-26 Expected type: NS f as Actual type: NS (NP f0) ('[] : as0) • In the expression: Here Nil In an equation for ‘HereNil’: HereNil = Here Nil • Relevant bindings include $bHereNil :: NS f as (bound at hs/457.hs:11:9) | 11 | pattern HereNil = Here Nil | ^^^^^^^^ hs/457.hs:11:24: error: • Kind mismatch: cannot unify (f :: a -> *) with: NP a0 :: [GHC.Types.Any] -> * Their kinds differ. Expected type: f a1 Actual type: NP a0 GHC.Types.Any • In the pattern: Nil In the pattern: Here Nil In the declaration for pattern synonym ‘HereNil’ | 11 | pattern HereNil = Here Nil | ^^^ Failed, no modules loaded. Prelude> }}} It can be given a pattern signature, my question is can this not be inferred {{{#!hs -- pattern HereNil :: NS (NP f) ('[]:as) pattern HereNil :: () => (nil_as ~ ('[]:as)) => NS (NP f) nil_as pattern HereNil = Here Nil }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15685 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15685: Pattern signature not inferred -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 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 Iceland_jack): It can be more general with a heterogeneous equality `(~~)`, can `NP f` be "delayed" as well? This is the limit of my knowledge {{{#!hs pattern HereNil :: () => (nil_as ~~ ('[]:as)) => NS (NP f) nil_as }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15685#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15685: Pattern signature not inferred -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 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 goldfire): While I can't say that the synonym should be accepted, the fact that `Any` appears in the error message is almost certainly wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15685#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15685: Pattern signature not inferred -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 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): OK I see what is happening. * There really is an error in the pattern synonym (see below). * But instead of failing, we just added some constraints to solve "later", and continued. * "Continued" means that we did a `zonkTcTypeToType` (in `tc_patsyn_finish`) which defaulted a unification variable to `Any`. I'll fix that; essentially we should not attempt to continue if there are any unsolved constraints from this pattern synonym. The error is a classic GADT one. Here is a simpler example: {{{ data T a b where T1 :: (a~Int) => b -> T a b pattern TX <- T1 True }}} We start with an overall pattern type of `T alpha beta`. Then, under the pattern match of `T1` we need `beta ~ Bool`, and that fails with {{{ T15685.hs:21:17: error: * Couldn't match expected type `b' with actual type `Bool' `b' is untouchable inside the constraints: a ~ Int bound by a pattern with constructor: T1 :: forall a b. (a ~ Int) => b -> T a b, in a pattern synonym declaration at T15685.hs:21:14-20 `b' is a rigid type variable bound by the inferred type of TX :: T a b at T15685.hs:21:9-10 Possible fix: add a type signature for `TX' }}} And indeed if we add a signature {{{ pattern TX :: T a Bool -- or pattern TX :: () => (a~Int) => T a Bool }}} then all is well. The example in the ticket is more complicated, because the untouchable variable is a ''kind'' variable. So the error that is now reported (after fixing the `Any` stuff) is {{{ T15685.hs:17:25: error: * Kind mismatch: cannot unify (f :: k -> *) with: NP a0 :: [*] -> * Their kinds differ. Expected type: f a Actual type: NP a0 b0 * In the pattern: Nil In the pattern: Here Nil In the declaration for pattern synonym `HereNil' }}} There is actually ''another'', separate kind-level error, which says that `k ~ [*]` is insoluble, because `k` is untoucahble. But currently we suppress the kind-level error in favour of the type-level error. TL;DR: * You need a pattern signature. That's by-design. * But the `Any` business is bogus, and I'll fix that. * The same fix also gets rid of the confusing error about `f ~~ NP f0`. This was is also the result of "carrying on" too much; it comes from the 'builder' for `HereNil` which we should not even attempt to typecheck if there is an earlier error. * The remaining kind error is correct; but not a very good error message. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15685#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15685: Pattern signature not inferred
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler | Version: 8.6.1
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 Simon Peyton Jones
#15685: Pattern signature not inferred -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | patsyn/should_fail/T15685 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => patsyn/should_fail/T15685 Comment: See post-commit comment on #15692 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15685#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15685: Pattern signature not inferred -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.2 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | patsyn/should_fail/T15685 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: 8.6.1 => 8.6.2 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15685#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15685: Pattern signature not inferred -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.2 Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | patsyn/should_fail/T15685 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.6` with 3e050064511ce67ee9150d51cb9db487187be39e. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15685#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC