SizeUnsolvedConstraintsInTypeSignature.agda

{-# OPTIONS --sized-types #-}
-- {-# OPTIONS -v tc.size.solve:20 -v tc.decl.ax:10 #-}
module SizeUnsolvedConstraintsInTypeSignature where

open import Common.Size

data Nat : (i : Size) -> Set where
  Z : {i : Size} -> Nat (↑ i)
  S : {i : Size} -> Nat i → Nat (↑ i)

one1 : (i : Size) → Nat (↑ (↑ i))
one1 i = S Z

one2 : (i : Size) → Nat (↑ (↑ (↑ i)))
one2 i = S Z

postulate
  _≡_   : {A : Set} → A → A → Set
  works : (i : Size) → one2 i ≡ one1 i

  bug   : (i : Size) → one1 i ≡ one2 i
  -- bug caused an interal error due to absense of range info
  -- should not print a proper error message (or better, work!)