Motivation

!3583 motivates me to actually write a feature request. Currently, there are type-level Nats, but I would like to have actual type-level floats. I am currently writing a linear-algebra library where I want to track certain things like the basis on the type-level and I would need to cross the type/term or term/type boundary (and the term-representation is via floats).

Proposal

Some relevant discussion can be found on #8697, where the focus is on rationals and not on floats, but I think both can go hand in hand. I think to implement such a feature one would need to figure out the parsing and adding floats to type-lits, but i am not a ghc-developer so I am not sure.

Ideally, I would imagine something like:

data Blah (num:: Float) = Blah

f :: forall num. KnownFloat num => Blah num -> Float
f = ...

g = f @1.3