Pattern synonym, (a::k) cannot be written (a::N) given (k ~ N)
I was trying to create a pattern synonym that matches TypeRep (a::k)
when k ~ N
, witnessing the equality and returning the representation.
This works fine:
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications #-}
import Type.Reflection
import Data.Kind
foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)
foo krep rep = do
HRefl <- eqTypeRep krep (typeRepKind rep)
pure (HRefl, rep)
data N = O | S N
pattern Bloop :: forall (a::k). () => N~k => TypeRep (a::k) -> TypeRep (a::k)
pattern Bloop rep <- (foo (typeRep @N) -> Just (HRefl, rep :: TypeRep (a::N)))
where Bloop rep = rep
Note that I have annotated rep :: TypeRep (a::N)
in the view pattern, which is the first argument to Bloop
.
Let's reflect that in the type
-- error:
-- • Expected kind ‘N’, but ‘a’ has kind ‘k’
-- • In the first argument of ‘TypeRep’, namely ‘(a :: N)’
-- In the type ‘TypeRep (a :: N) -> TypeRep (a :: k)’
-- |
-- 15 | pattern Bloop :: forall (a::k). () => N ~ k => TypeRep (a::N) -> TypeRep (a::k)
-- | ^
pattern Bloop :: forall (a::k). () => N~k => TypeRep (a::N) -> TypeRep (a::k)
pattern Bloop rep <- (foo (typeRep @N) -> Just (rep, HRefl))
where Bloop rep = rep
Oh no, GHC complains that a::k
(not a::N
) but we have local knowledge that N ~ k
. I know the rules for kinds are weird so I don't know if this is intended.
A way around this is quantifying over an existential variable that is heterogeneously equal to a
:
pattern Bloop :: forall (a::k). () => forall (n::N). a~~n => TypeRep (n::N) -> TypeRep (a::k)
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |