Can't parse `forall j -> @m k`
I was originally startled to discover that this typechecks:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
module Bug where
import Data.Kind
type family F1 (k :: Type) :: k where {}
type family F2 :: forall (k :: Type) -> k where
F2 = F1
However, it turns out that this is actually fine. If you run :info F2
in GHCi with -fprint-explicit-matchabilities -fprint-explicit-kinds
enabled, it will reveal the full story:
λ> :set -fprint-explicit-matchabilities -fprint-explicit-kinds
λ> :info F2
type F2 :: forall {t :: GHC.Types.Matchability}. forall k ->{t} k
type family F2 @{t} where
F2 @{'GHC.Types.Unmatchable} = F1
-- Defined at Bug.hs:11:1
All that's going on is that the F2 = F1
implicitly matches t
to be Unmatchable
. That's fine, although I like to be explicit about this sort of thing in type families. When I tried to make this explicit:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
module Bug where
import Data.Kind
type family F1 (k :: Type) :: k where {}
type family F2 :: forall t. forall (k :: Type) -> @t k where
F2 @{Unmatchable} = F1
It no longer parses!
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:51: error: parse error on input ‘@’
|
12 | type family F2 :: forall t. forall (k :: Type) -> @t k where
| ^
Would it be difficult to make this parse?