GitLab

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