{-# OPTIONS --type-in-type #-} module PatternSynonymsErrorLocationRHS where data _≡_ {A : Set}(a : A) : A -> Set where refl : a ≡ a infixr 2 _,_ record Unit : Set where data Sigma (A : Set)(B : A -> Set) : Set where _,_ : (fst : A) -> B fst -> Sigma A B -- Prod does not communicate guardedness Prod : (A B : Set) -> Set Prod A B = Sigma A \ _ -> B data Empty : Set where data ListTag : Set where nil cons : ListTag {-# NO_TERMINATION_CHECK #-} List : (A : Set) -> Set List A = Sigma ListTag T where T : ListTag -> Set T nil = Unit T cons = Sigma A \ _ -> List A infix 5 _∷_ pattern [] = nil , _ pattern _∷_ x xs = cons , x , xs -- FAILS: pattern x ∷ xs = cons , x , xs data TyTag : Set where base arr : TyTag {-# NO_TERMINATION_CHECK #-} Ty : Set Ty = Sigma TyTag T where T : TyTag -> Set T base = Unit T arr = Sigma Ty \ _ -> Ty -- Prod Ty Ty infix 10 _⇒_ pattern ★ = base , _ pattern _⇒_ A B = arr , A , B Context = List Ty data NatTag : Set where zero succ : NatTag Var : (Gamma : Context)(C : Ty) -> Set Var [] C = Empty Var (cons , A , Gamma) C = Sigma NatTag T where T : NatTag -> Set T zero = A ≡ C T succ = Var Gamma C pattern vz = zero , refl pattern vs x = succ , x idVar : (Gamma : Context)(C : Ty)(x : Var Gamma C) -> Var Gamma C idVar [] _ () idVar (A ∷ Gamma) C (zero , proof) = zero , proof -- idVar (A ∷ Gamma) C vz = vz idVar (A ∷ Gamma) C (vs x) = vz -- vs (idVar Gamma C x)