SizedTypesScopeViolationInMeta.agda

{-# OPTIONS  --sized-types --show-implicit #-} 

module SizedTypesScopeViolationInMeta where

open import Size

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

-- exposing a bug in size constraint solving

-- *** Exception: Inconsistent meta: _73 [[CtxId 420],[CtxId 418]]
A : Set1
A = (Id : {i : Size} -> Nat {_} -> Set)
    (k : Size)(m : Nat {↑ k}) -> Id {k} m 
    ->
    (j : Size)(n : Nat {j}) -> Id {j} n 

{-
mutual

--   id : {i : Size} -> Nat {_} -> Nat {i}  -- FAILS
  id : {i : Size} -> Nat {i} -> Nat {i} 
  id x = x

  succ : {i : Size} -> Nat {i} -> Nat {↑ i}
  succ x = suc (id x)
-}