Opened 12 months ago

Closed 11 months ago

## #15685 closed bug (fixed)

# Pattern signature not inferred

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.6.2 |

Component: | Compiler | Version: | 8.6.1 |

Keywords: | PatternSynonyms | Cc: | |

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: |

### Description

Should this pattern synonym declaration fail,

{-# 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

-- pattern HereNil :: NS (NP f) ('[]:as) pattern HereNil :: () => (nil_as ~ ('[]:as)) => NS (NP f) nil_as pattern HereNil = Here Nil

### Change History (7)

### comment:2 Changed 12 months ago by

While I can't say that the synonym should be accepted, the fact that `Any`

appears in the error message is almost certainly wrong.

### comment:3 Changed 12 months ago by

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.

### comment:5 Changed 12 months ago by

Status: | new → merge |
---|---|

Test Case: | → patsyn/should_fail/T15685 |

See post-commit comment on #15692

### comment:6 Changed 12 months ago by

Milestone: | 8.6.1 → 8.6.2 |
---|

### comment:7 Changed 11 months ago by

Resolution: | → fixed |
---|---|

Status: | merge → closed |

Merged to `ghc-8.6`

with 3e050064511ce67ee9150d51cb9db487187be39e.

**Note:**See TracTickets for help on using tickets.

It can be more general with a heterogeneous equality

`(~~)`

, can`NP f`

be "delayed" (provided constraint) as well? This is the limit of my knowledge