#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:1 Changed 12 months ago by Iceland_jack

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

pattern HereNil :: () => (nil_as ~~ ('[]:as)) => NS (NP f) nil_as
Last edited 12 months ago by Iceland_jack (previous) (diff)

comment:2 Changed 12 months ago 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.

comment:3 Changed 12 months ago 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.

comment:4 Changed 12 months ago by Simon Peyton Jones <simonpj@…>

In 9ebfa03/ghc:

Fail fast on pattern synonyms

We were recovering too eagerly from errors in pattern-synonym
type inference, leading to a cascade of confusing follow up errors
(Trac #15685, #15692).

The underlying issue is that a pattern synonym should have a closed,
fixed type, with no unification variables in it.  But it wasn't!

Fixing this made me change the interface to simplifyInfer slightly.
Instead of /emitting/ a residual implication constraint, it
now /returns/ it, so that the caller can decide what to do.

comment:5 Changed 12 months ago by simonpj

Status: newmerge
Test Case: patsyn/should_fail/T15685

See post-commit comment on #15692

comment:6 Changed 12 months ago by RyanGlScott

Milestone: 8.6.18.6.2

comment:7 Changed 11 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.