If we have a datatype inside a module parameterized by a type, we can define a looping term by mutually applying the module to the term itself:
module M (X : Set) where data X' : Set where Bad : Set open M Bad Bad = X' -- Bad = M.X' Bad
If the datatype is replaced with a postulate (postulate X' : Set), then the termination checker correctly rejects the example.
We can also derive false by using the above method to define a non-positively recursive datatype:
{-# OPTIONS --safe #-}
data ⊥ : Set where
module M (X : Set) where
data ¬X : Set where
neg : (X → ⊥) → ¬X
Bad : Set
open M Bad
Bad = ¬X
bad : Bad → ⊥
bad (neg f) = f (neg f)
oops : ⊥
oops = bad (neg bad)
gallais, jespercockx, arthur-adjedj, marvinborner, andreasabel and 1 more
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4