#10776: DataKinds promotion of String -> Symbol and Natural -> Nat -------------------------------------+------------------------------------- Reporter: htebalaka | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by htebalaka: Old description:

Exactly what it says on the tin. It would be nice if the following would compile:

{{{#!hs {-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

import GHC.TypeLits import GHC.Natural

data X = X String Natural

data Y :: X -> * where Y :: Y (X "hello" 4) }}}

I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case.

New description: Exactly what it says on the tin. It would be nice if the following would compile: {{{#!hs {-# LANGUAGE DataKinds, KindSignatures, GADTs #-} import GHC.TypeLits import GHC.Natural data X = X String Natural data Y :: X -> * where Y :: Y ('X "hello" 4) }}} I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10776#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10776: DataKinds promotion of String -> Symbol and Natural -> Nat -------------------------------------+------------------------------------- Reporter: htebalaka | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dmcclean): A hearty amen on this one, especially unifying `Natural` with `Nat`. Regarding the `String` objection perhaps it would be better to merely flesh out `Symbol` at the term level? With an `IsString` instance and so forth? Because as mentioned unifying it with `String` is problematic since `String` is a type synonym for a list of characters. I also agree with Richard's comments regarding the desirability of type- level literals of all stripes (or at least other stripes). I'm not sure if floating-point numbers or characters specifically are useful, but integers and rationals most definitely are of use to the `dimensional` library. We have home-brewed ones, but it is a lot of machinery, isn't interoperable with the few other flavors of home-brewed ones on the market, and isn't the lifted version of `Rational` or `Integer` so you can't use the lifted kinds that go with the types of term-level structures that include rational or integers. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10776#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10776: DataKinds promotion of String -> Symbol and Natural -> Nat -------------------------------------+------------------------------------- Reporter: htebalaka | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11342 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * related: => #11342 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10776#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler