toRational for CReal?

[arrowd]

I see there is a implementation for instance Real CReal, but its toRational implementation is commented out:

 -- toRational x@(CR x') = x' n % 2^n where n = digitsToBits digits

  toRational _ = error "CReal.toRational"

What's wrong with it?

[cartazio]

constructive reals Cant be turned into a finite representation in finite time.

a simple example is PI, clearly a Computable / constructive real.... theres no rational number equal to pi!

more broadly, theres no decidable way to know if theres a finite rational rep from the current CReal rep