[GHC] #13186: Change EvNum to EvNum :: Natural -> EvLit
#13186: Change EvNum to EvNum :: Natural -> EvLit -------------------------------------+------------------------------------- Reporter: phadej | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #8306 #8412 | #13181 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13186 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13186: Change EvNum to EvNum :: Natural -> EvLit -------------------------------------+------------------------------------- Reporter: phadej | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8306 #8412 | Differential Rev(s): #13181 | Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13186#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13186: Change EvNum to EvNum :: Natural -> EvLit -------------------------------------+------------------------------------- Reporter: phadej | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8306 #8412 | Differential Rev(s): #13181 | Wiki Page: | -------------------------------------+------------------------------------- Comment (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/com... And then we could use `minusNaturalMaybe` https://github.com/ghc/ghc/blob/ff9355e48d0cb04b3adf26e27e12e128f79618f4/com... here, i.e. unify `Natural` and `KnownNat` handling by ''using same functions''. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13186#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13186: Change EvNum to EvNum :: Natural -> EvLit -------------------------------------+------------------------------------- Reporter: phadej | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8306 #8412 | Differential Rev(s): #13181 | Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13186#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC