GitLab

With the latest version of type applications in patterns, I can write the following:

pattern ThisNat :: forall (i :: Nat). KnownNat i => Nat
pattern ThisNat <- ( ( natVal' @i proxy# == ) -> True )
  where
    ThisNat = natVal' @i proxy#

example :: Nat -> String
example = \case
  ThisNat @3 -> "matched on 3"
  ThisNat @7 -> "matched on 7"
  ThisNat @4 -> "matched on 4"
  ThisNat @3 -> "matched on second 3"
  _          -> "fallthrough"

vals :: [ String ]
vals = map example [ 0 .. 8 ]
-- > vals
-- ["fallthrough","fallthrough","fallthrough"
-- ,"matched on 3","matched on 4","fallthrough"
-- ,"fallthrough","matched on 7","fallthrough"]

However, if I try to write a type application when defining the pattern, I get a parse error

pattern ThisNat :: forall (i :: Nat). KnownNat i => Nat
pattern ThisNat @i <- ( ( natVal' @i proxy# == ) -> True )
  where
    ThisNat = natVal' @i proxy#

error: parse error on input `@'
    |
    | pattern ThisNat @i <- ( ( natVal' @i proxy# == ) -> True )
    |                 ^

I find this asymmetry somewhat surprising. As a point of comparison (not necessarily very relevant), when visible kind application was added to GHC, we were able to use the feature both at use sites of type families but also at definition sites:

type F :: forall k. k -> k -- (really foreach k. k -> k)
type family F a where
  F @Nat  3    = 4
  F @Bool True = False

Note that, on the other hand, when trying to use a type application on the constructor, the following compiles OK:

pattern ThisNat :: forall (i :: Nat). KnownNat i => Nat
pattern ThisNat <- ( ( natVal' @i proxy# == ) -> True )
  where
    ThisNat @i = natVal' @i proxy#

whereas the following produces the error

pattern ThisNat :: forall (i :: Nat). KnownNat i => Nat
pattern ThisNat <- ( ( natVal' @i proxy# == ) -> True )
  where
    ThisNat @j = natVal' @j proxy#

 error: Not in scope: type variable `j'
    |
    |     ThisNat @j = natVal' @j proxy#
    |

which is quite different from the error that the following program produces (which doesn't change depending on whether we use i or j):

thisNat :: forall i. KnownNat i => Nat
thisNat @j = natVal' @j proxy#

 error:
    Parse error in pattern: thisNat @j
    Type applications in patterns are only allowed on data constructors.
    |
    | thisNat @j = natVal' @j proxy#
    | ^^^^^^^

None of this is at all serious, but I thought the inconsistencies in the error messages could be worth pointing out.