Use of Non-terminating Function in Data Declaration Makes Typechecker Loop

[emekoi]

Use of Non-terminating Function in Data Declaration Makes Typechecker Loop

[andreasabel]

I am closing this as duplicate of #1270.

[andreasabel]

Yes, that's why we have a termination checker. But it does not run until the mutual block is complete. Your example opens an implicit mutual block with the data signature Flip' which is only closed until the data definition Flip' is provided.

Workaround is to use the {-# NON_TERMINATING #-} pragma (insert before Flip). This stops Flip from being unfolded.

[emekoi]

Ah, so this is the intended (unavoidable) behavior? Are definitions lifted out of mutual blocks if there isn't an actual dependency? Because the following terminates just fine:

data Unit : Set where

data Flip' (x : Unit) : (y : Unit) -> Set

Flip : Unit -> Unit -> Set
Flip x y = Flip y x

data Flip' a where

EDIT: Nevermind, we don't use Flip here so when the termination checker runs, it doesn't get stuck trying to evaluate Flip since it's never used.

[andreasabel]

Ah, so this is the intended (unavoidable) behavior?

Yes, somewhat unfortunately it is hard to fix:

• #1270

Are definitions lifted out of mutual blocks if there isn't an actual dependency?

They formally stay in the mutual block, but the termination checker computes the actual dependencies.

Because the following terminates just fine:

Yes here you get the expected termination error for Flip.