Opened 23 months ago

Last modified 23 months ago

#13186 new feature request

Change EvNum to EvNum :: Natural -> EvLit

Reported by: phadej Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: Cc: bgamari
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #8306 #8412 #13181 Differential Rev(s):
Wiki Page:

Description

Currently we carry Nat kind as an Integer internally.

Just changing the type of EvNum (and related isomorphic types like HsTyLit etc) does pretty far. The core problem is that we should be able to output Natural literals into Core.

Also this would need change to parser, to accept only Naturals in types. Currently negative literals are caught in the renamer (due the fact that template-haskell might inject negative integers as well).

This will propagate to template-haskell, changing TyLit there as well.

Change History (3)

comment:1 Changed 23 months ago by mpickering

This seems very invasive but for what? The situation where the internal representation is an Integer but the representation exposed is a Natural seems much easier to implement.

comment:2 Changed 23 months ago by phadej

On the other hand:

This smells funny. Why is there so much Integer here? Why is a conversion from Integer to Natural being put in such deep code? I'm clearly missing something!

https://phabricator.haskell.org/D3024

AFAICS, it's totally possible to thread Natural thru the pipeline, we do very little calculations with type level nats (in a single module), everywhere else the value is just passed forward. Like in https://github.com/ghc/ghc/blob/ff9355e48d0cb04b3adf26e27e12e128f79618f4/compiler/typecheck/TcInteract.hs#L2106

And then we could use minusNaturalMaybe https://github.com/ghc/ghc/blob/ff9355e48d0cb04b3adf26e27e12e128f79618f4/compiler/typecheck/TcTypeNats.hs#L691 here, i.e. unify Natural and KnownNat handling by using same functions.

comment:3 Changed 23 months ago by phadej

Currently we can get:

Prelude> :set -XDataKinds -XNegativeLiterals 
Prelude> :m +Data.Proxy 
Prelude Data.Proxy> Proxy :: Proxy (-1)

Even this case could (and should?) be ruled out in parser, thru template-haskell you can still inject negative integers. Thus the workaround fix is currently in the renamer.

Note: See TracTickets for help on using tickets.