diff --git a/testsuite/tests/simplCore/should_compile/T15186.hs b/testsuite/tests/simplCore/should_compile/T15186.hs new file mode 100644 index 0000000000000000000000000000000000000000..c04de6adfab97c099e6b84386848ab23a34fcb5c --- /dev/null +++ b/testsuite/tests/simplCore/should_compile/T15186.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PatternSynonyms #-} +module Bar (pattern PointerExpr) where + +import T15186A + +------------------------------------------------------------------------------- + +pattern PointerExpr :: Expr tp +pattern PointerExpr <- + App (RollRecursive (EmptyAssn :> BVRepr) (App _)) + +------------------------------------------------------------------------------- + +data CrucibleType where + RecursiveType :: Ctx CrucibleType -> CrucibleType + +data TypeRepr (tp :: CrucibleType) where + BVRepr :: TypeRepr tp + TypeReprDummy :: TypeRepr tp + +data App (f :: CrucibleType -> *) (tp :: CrucibleType) where + RollRecursive :: !(Assignment TypeRepr ctx) + -> !(Expr tp) + -> App f ('RecursiveType ctx) + +data Expr (tp :: CrucibleType) + = App !(App Expr tp) + | ExprDummy diff --git a/testsuite/tests/simplCore/should_compile/T15186A.hs b/testsuite/tests/simplCore/should_compile/T15186A.hs new file mode 100644 index 0000000000000000000000000000000000000000..472d01c0affa1b782c6a4fd73600eabe380e00f7 --- /dev/null +++ b/testsuite/tests/simplCore/should_compile/T15186A.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +module T15186A (Ctx, Assignment, pattern EmptyAssn, pattern (:>)) where + +import Data.Kind (Type) + +data Ctx k + = EmptyCtx + | Ctx k ::> k + +type SingleCtx x = 'EmptyCtx '::> x + +type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k where + x <+> 'EmptyCtx = x + x <+> (y '::> e) = (x <+> y) '::> e + +data Height = Zero | Succ Height + +data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where + Empty :: BinomialTree h f 'EmptyCtx + PlusOne :: !Int + -> !(BinomialTree ('Succ h) f x) + -> !(BalancedTree h f y) + -> BinomialTree h f (x <+> y) + PlusZero :: !Int + -> !(BinomialTree ('Succ h) f x) + -> BinomialTree h f x + +newtype Assignment (f :: k -> *) (ctx :: Ctx k) + = Assignment (BinomialTree 'Zero f ctx) + +data AssignView f ctx where + AssignEmpty :: AssignView f 'EmptyCtx + AssignExtend :: Assignment f ctx + -> f tp + -> AssignView f (ctx '::> tp) + +data DropResult f (ctx :: Ctx k) where + DropEmpty :: DropResult f 'EmptyCtx + DropExt :: BinomialTree 'Zero f x + -> f y + -> DropResult f (x '::> y) + +data BalancedTree h (f :: k -> Type) (p :: Ctx k) where + BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x) + BalPair :: !(BalancedTree h f x) + -> !(BalancedTree h f y) + -> BalancedTree ('Succ h) f (x <+> y) + +bal_drop :: forall h f x y + . BinomialTree h f x + -> BalancedTree h f y + -> DropResult f (x <+> y) +bal_drop t (BalLeaf e) = DropExt t e +bal_drop _ (BalPair {}) = undefined + +bin_drop :: forall h f ctx + . BinomialTree h f ctx + -> DropResult f ctx +bin_drop Empty = DropEmpty +bin_drop (PlusZero _ u) = bin_drop u +bin_drop (PlusOne s t u) = + let m = case t of + Empty -> Empty + _ -> PlusZero s t + in bal_drop m u + +viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx +viewAssign (Assignment x) = + case bin_drop x of + DropEmpty -> AssignEmpty + DropExt t v -> AssignExtend (Assignment t) v + +pattern EmptyAssn :: () => ctx ~ 'EmptyCtx => Assignment f ctx +pattern EmptyAssn <- (viewAssign -> AssignEmpty) + +pattern (:>) :: () => ctx' ~ (ctx '::> tp) => Assignment f ctx -> f tp -> Assignment f ctx' +pattern (:>) a v <- (viewAssign -> AssignExtend a v) diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T index 1bc42afb3616bdd9b5092eca3b18b1d02c0dabb7..a430521c89ffd30749a9c2d15a4efafb7705f5f4 100644 --- a/testsuite/tests/simplCore/should_compile/all.T +++ b/testsuite/tests/simplCore/should_compile/all.T @@ -315,3 +315,4 @@ test('T15002', [ req_profiling ], compile, ['-O -fprof-auto -prof']) test('T15005', normal, compile, ['-O']) # we omit profiling because it affects the optimiser and makes the test fail test('T15056', [extra_files(['T15056a.hs']), omit_ways(['profasm'])], multimod_compile, ['T15056', '-O -v0 -ddump-rule-firings']) +test('T15186', expect_broken(15186), multimod_compile, ['T15186', '-v0'])