Instantiation of inference variables might be too eager

[ice1000]

Given this code:

\data Maybe (A : \Type) | just A | nothing
\func NatInf' => Maybe Nat
\func zero' => just zero

\func suc' (n : NatInf') : NatInf'
  | just a => just (suc a)
  | nothing => nothing

\func infinity' => nothing

  \data NatInf
    | nzero
    | infinity
    | nsucc NatInf
    | ntrunc I \with {
      | left => infinity
      | right => nsucc infinity
    }

  \func to (n : NatInf) : NatInf'
    | nzero => zero'
    | infinity => infinity'
    | nsucc n => suc' (to n)
    | ntrunc i => infinity'

Arend rejects this code with this little poem:

[ERROR] NatWithInfinity.ard:39:19: Cannot infer parameter 'A'
  Candidates are: Nat
  Since types of the candidates are not less than or equal to the expected type
  Expected type: \Prop
    Actual type: \Set0

It's worked around by manually giving infinity' a return type annotation NatInf'. I guess we should not need to do so in general. Maybe Arend inferred the type of infinity' as something weird, but I'd expect it to be {A : \Type} -> Maybe A.