Type rationals

I've used GHC's Type Nats to implement my own type level rationals (code below). This works fine, but the syntax is a little funky because you have to write out the number as a fraction. For example, you must write 13/10 instead of 1.3; or even worse, 13/1 instead of 13. It would be nice to just write the decimal notation.

I only see one potential problem with this feature: the dot in the decimal notation could interfere with the dot in forall statements. I guess this can be parsed unambiguously, but maybe not.

data Frac = Frac Nat Nat

data instance Sing (n::Frac) = SFrac Integer Integer

instance (SingI a, SingI b) => SingI ('Frac a b) where
    sing = SFrac (fromSing (sing :: Sing a)) (fromSing (sing :: Sing b))

instance Fractional r => SingE (Kind :: Frac) r where
    fromSing (SFrac a b) = fromIntegral a/fromIntegral b

type (/) a b = 'Frac a b

Trac metadata

Trac field	Value
Version	7.6.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture