[Agda] internal error with sized types

[Samuel Gélineau]

Hi,

I know that sized types can be used to tag transformations which don't
increase the size. Can they also be used to tag transformations which
strictly decrease the size? I've tried to figure out using the code
below, but it caused an internal error. So I guess this message
doubles as a bug report.

– Samuel Gélineau


{-# OPTIONS --sized-types #-}
module Main where

open import Size
open import Data.Unit
open import Data.Sum

-- Nat, but with sized types
data N : {i : Size} → Set where
  z : {i : Size} → N {↑ i}
  s : {i : Size} → N {i} → N {↑ i}

-- strictly decreasing!
case : {i : Size} → N {↑ i} → ⊤ ⊎ N {i}
case z = inj₁ tt
case (s x) = inj₂ x

-- doesn't pass termination checking, but compiles.
-- notice that the size annotation is commented out.
pass : {i : Size} → N {-i-} → ⊤
pass x with case x
... | {- z -}   inj₁ _ = tt
... | {- s y -} inj₂ y = pass y

-- same function, but making use of the size annotation.
-- should hopefully pass termination checking, but crashes:
--   An internal error has occurred. Please report this as a bug.
--   Location of the error: src/full/Agda/TypeChecking/Constraints.hs:103
fail : {i : Size} → N {i} → ⊤
fail x with case x
... | {- z -}   inj₁ _ = tt
... | {- s y -} inj₂ y = fail y