summaryrefslogtreecommitdiff
path: root/testsuite/tests/patsyn/should_fail/T15695.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/patsyn/should_fail/T15695.hs')
-rw-r--r--testsuite/tests/patsyn/should_fail/T15695.hs48
1 files changed, 48 insertions, 0 deletions
diff --git a/testsuite/tests/patsyn/should_fail/T15695.hs b/testsuite/tests/patsyn/should_fail/T15695.hs
new file mode 100644
index 0000000000..de8035c728
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15695.hs
@@ -0,0 +1,48 @@
+{-# Language RankNTypes, PatternSynonyms, DataKinds, PolyKinds, GADTs,
+ TypeOperators, MultiParamTypeClasses, TypeFamilies,
+ TypeSynonymInstances, FlexibleInstances, InstanceSigs, FlexibleContexts #-}
+
+{-# Options_GHC -fdefer-type-errors #-}
+
+module T15695 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data TyVar :: Type -> Type -> Type where
+ VO :: TyVar (a -> as) a
+ VS :: TyVar as a -> TyVar (b -> as) a
+
+data NP :: (k -> Type) -> ([k] -> Type) where
+ Nil :: NP f '[]
+ (:*) :: f a -> NP f as -> NP f (a:as)
+
+data NS :: (k -> Type) -> ([k] -> Type) where
+ Here :: f a -> NS f (a:as)
+ There :: NS f as -> NS f (a:as)
+
+infixr 6 :&:
+data Ctx :: Type -> Type where
+ E :: Ctx(Type)
+ (:&:) :: a -> Ctx(as) -> Ctx(a -> as)
+
+data NA a
+
+type SOP(kind::Type) code = NS (NP NA) code
+
+data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
+ AO :: a -> ApplyT(Type) a E
+ AS :: ApplyT(ks) (f a) ctx
+ -> ApplyT(k -> ks) f (a:&:ctx)
+
+from' :: ApplyT(Type -> Type -> Type) Either ctx -> NS (NP NA) '[ '[VO] ]
+from' (ASSO (Left a)) = Here (a :* Nil)
+from' (ASSO (Right b)) = There (Here undefined)
+
+pattern ASSO
+ :: () =>
+ forall (ks :: Type) k (f :: k -> ks) (a1 :: k) (ks1 :: Type) k1 (f1 :: k1 -> ks1) (a2 :: k1) a3.
+ (kind ~ (k -> k1 -> Type), a ~~ f, b ~~ (a1 :&: a2 :&: E),
+ f a1 ~~ f1, f1 a2 ~~ a3) =>
+ a3 -> ApplyT kind a b
+pattern ASSO a = AS (AS (AO a))