Slight inconsistencies in error messages with type applications in patterns
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.