blob: b7f7db4d8a5e40f46942194779963e2602fc47fa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds #-}
module T14498 where
import Type.Reflection
import Data.Kind
data Dict c where Dict :: c => Dict c
asTypeable :: TypeRep a -> Dict (Typeable a)
asTypeable rep =
withTypeable rep
Dict
pattern Typeable :: () => Typeable a => TypeRep a
pattern Typeable <- (asTypeable -> Dict)
where Typeable = typeRep
data N = O | S N
type SN = (TypeRep :: N -> Type)
pattern SO = (Typeable :: TypeRep (O::N))
pattern SS ::
forall k' (t :: k').
()
=> forall kk (a :: kk -> k') (n :: kk).
(t ~ a n)
=>
TypeRep n -> TypeRep t
pattern SS n <- (App (Typeable :: TypeRep (a ::kk -> k')) n)
|
