blob: 6c8326733cab72b1c590b9a341d88ee05f6ee862 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes,
PolyKinds, ScopedTypeVariables, DataKinds, TypeOperators,
TypeApplications, TypeFamilies, TypeFamilyDependencies,
StandaloneKindSignatures #-}
module T14507 where
import Type.Reflection
import Data.Kind
foo :: TypeRep a -> (Bool :~~: k, TypeRep a)
foo rep = error "urk"
type SING :: k -> Type
type family SING where
SING = (TypeRep :: Bool -> Type)
pattern RepN :: forall kk (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
, tr :: TypeRep (a::Bool)))
pattern SO x <- RepN (id -> x)
|