recursive core tc failure

au-ts / cogent

Cogent Project

Other

158 stars 26 forks source link

Closed zilinc closed 4 years ago

zilinc commented 4 years ago

type ListNode a = rec t { l: < Nil | Cons (a,t) > }

size : (ListNode ())! -> U8
size r {l} = l | Nil -> 0
               | Cons (a,t) -> size t

results in Internal TC failed: GUARD: take: sigil not readonly.

Also, if I define size : all a. (ListNode a)! -> U8 we still have the a! :=: ?14! problem. Hasn't it been fixed by the sink-float stage?

zilinc commented 4 years ago

see #356