[Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)

[Apostolis Xekoukoulotakis]

Here is a simple program that works in Idris but not in agda. Is there a
way to make it work in agda?

agda:

```

module terminate where
open import Data.Nat
fn : ℕ → ℕfn zero    = zerofn (suc k) = zero
gn : ℕ → ℕgn x = zero
data Test : ℕ → Set where
  Tist : Test zero
  Tost : (n : ℕ) → Test (fn n)
tn : (n : ℕ) → Test (fn n) → ℕtn zero Tist = zerotn zero (Tost zero) =
zerotn zero (Tost (suc k)) = zerotn (suc y) x = {!!}


```

idris:

```
module Main

%default total

fn : Nat -> Nat
fn Z = Z
fn (S k) = Z

gn : Nat -> Nat
gn x = Z


data Test : Nat -> Type where
  Tost : (n : Nat) -> Test $ fn n
  Tist : Test Z


tn : (n : Nat) -> Test $ fn n -> Nat
tn Z Tist = ?tn_rhs_3
tn Z (Tost Z) = ?tn_rhs_3
tn Z (Tost (S k)) = ?tn_rhs_3
tn (S k) x = ?tn_rhs_2

```
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161211/00d88e5c/attachment.html