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