SizeInconsistentMeta4.agda 2.2 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657
  1. -- Andreas, 2012-02-24 example by Ramana Kumar
  2. {-# OPTIONS --sized-types #-}
  3. -- {-# OPTIONS --show-implicit -v tc.size.solve:20 -v tc.conv.size:15 #-}
  4. module SizeInconsistentMeta4 where
  5. open import Data.Nat using (ℕ;zero;suc) renaming (_<_ to _N<_)
  6. open import Data.Product using (_,_;_×_)
  7. open import Data.Product.Relation.Binary.Lex.Strict using (×-Lex; ×-transitive)
  8. open import Data.List using (List)
  9. open import Data.List.Relation.Binary.Lex.Strict using (Lex-<) renaming (<-transitive to Lex<-trans)
  10. open import Relation.Binary using (Rel;_Respects₂_;Transitive;IsEquivalence)
  11. open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
  12. open import Level using (0ℓ)
  13. open import Size using (Size;↑_)
  14. -- keeping the definition of Vec for the positivity check
  15. infixr 5 _∷_
  16. data Vec {a} (A : Set a) : ℕ → Set a where
  17. [] : Vec A zero
  18. _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
  19. {- produces different error
  20. data Lex-< {A : _} (_≈_ _<_ : Rel A Level.zero) : Rel (List A) Level.zero where
  21. postulate
  22. Lex<-trans : ∀ {P _≈_ _<_} →
  23. IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
  24. Transitive (Lex-< _≈_ _<_)
  25. -}
  26. postulate
  27. N<-trans : Transitive _N<_
  28. -- Vec : ∀ {a} (A : Set a) → ℕ → Set a
  29. Vec→List : ∀ {a n} {A : Set a} → Vec A n → List A
  30. data Type : Size → Set where
  31. TyApp : {z : Size} (n : ℕ) → (as : Vec (Type z) n) → Type (↑ z)
  32. <-transf : ∀ {z} → Rel (Type z) 0ℓ → Rel (ℕ × List (Type z)) 0ℓ
  33. <-transf _<_ = ×-Lex _≡_ _N<_ (Lex-< _≡_ _<_)
  34. infix 4 _<_
  35. data _<_ : {z : Size} → Rel (Type z) 0ℓ where
  36. TyApp<TyApp : ∀ {z} {n₁} {as₁} {n₂} {as₂} →
  37. <-transf (_<_ {z}) (n₁ , Vec→List as₁) (n₂ , Vec→List as₂) →
  38. _<_ {↑ z} (TyApp n₁ as₁) (TyApp n₂ as₂)
  39. <-trans : ∀ {z} → Transitive (_<_ {z})
  40. <-trans (TyApp<TyApp p) (TyApp<TyApp q) =
  41. TyApp<TyApp (×-transitive {_<₂_ = Lex-< _≡_ _<_}
  42. PropEq.isEquivalence
  43. (PropEq.resp₂ _N<_)
  44. N<-trans
  45. (Lex<-trans PropEq.isEquivalence (PropEq.resp₂ _<_) <-trans)
  46. p q)