
Hi Dominique, On 06/02/15 12:13, Dominique Devriese wrote:
Perhaps only for the sake of discussion: have you considered doing something at the type-level instead of using TH? I mean that you could change the type of 42 from `forall a. Num a => a` to `forall a. HasIntLiteral a '42 => a` where HasIntegerLiteral is a type class of kind `* -> 'Integer -> Constraint` and people can instantiate it for their types:
class HasIntegerLiteral (a :: *) (k :: 'Integer) where literal :: a
The desugarer could then just generate an invocation of "literal".
An advantage would be that you don't need TH (although you do need DataKinds and type-level computation). Specifically, type-checking remains decidable and you can do it in safe haskell and so on. I haven't thought this through very far, so there may be other advantages/disadvantages/glaring-holes-in-the-idea that I'm missing.
Interestingly, the string version of this would be remarkably similar to the IV class [1] that came up in the redesign of OverloadedRecordFields: class IV (x :: Symbol) a where iv :: a though in this case the plan was to have a special syntax for such literals (e.g. #x). It seems to me that what you would describe would work, and the avoidance of TH is a merit, but the downside is the complexity of implementing even relatively simple validation at the type level (as opposed to just reusing a term-level function). For Merijn's Even example I guess one could do something like this in current GHC: type family IsEven (n :: Nat) :: Bool where IsEven 0 = True IsEven 1 = False IsEven n = n - 2 instance (KnownNat n, IsEven n ~ True) => HasIntegerLiteral Even n where literal = Even (natVal (Proxy :: Proxy n)) but anything interesting to do with strings (e.g. checking that ByteStrings are ASCII) is rather out of reach at present. Adam [1] https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Redesig... -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/