Treat kind/type variables identically, demolish FKTV
[ghc.git] / testsuite / tests / patsyn / should_fail / T14507.hs
1 {-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes,
2 PolyKinds, ScopedTypeVariables, DataKinds, TypeOperators,
3 TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
4
5 module T14507 where
6
7 import Type.Reflection
8 import Data.Kind
9
10 foo :: TypeRep a -> (Bool :~~: k, TypeRep a)
11 foo rep = error "urk"
12
13 type family SING :: k -> Type where
14 SING = (TypeRep :: Bool -> Type)
15
16 pattern RepN :: forall kk (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
17 pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
18 , tr :: TypeRep (a::Bool)))
19
20 pattern SO x <- RepN (id -> x)
21