Re: Further custom type error questions

FWIW: I didn't realise that this kind of example was the point of TypeError being kind-polymorphic, thanks for the clarification. I don't see an easy way of encoding this using the simpler alternative I suggested, so my question is answered. In hindsight, the wiki does already show an example like this, so I must have missed this, sorry. Thanks, see you, Dominique PS: I would still be interested if anyone has thoughts about the TypeWarning thing I suggested... 2015-11-17 12:31 GMT+01:00 Roman Cheplyaka :

Iavor, Ben, et al.:

How about much simpler

type family Head (a :: [k]) :: k where Head (x ': xs) = x Head '[] = Error "Empty list"

Can this be expressed through Error-as-constraint?

On 11/17/2015 02:09 AM, Iavor Diatchki wrote:

...

Hello,

I imagine people wanting to do things as in the example below. If we were to use only `TypeError` constraints, then we'd have to mostly use the class system to do type-level evaluation. It doesn't seem obvious how to do that with just `TypeError` of kind constraint, unless all evaluation was to happen using the class system.

-Iavor PS: Interestingly, this example reveals a bug with GHC's new warning about unused constraints, where the `OffsetOf` constant on `get` is reported as unnecessary... I'll file a bug.

{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-}

import GHC.TypeLits import Data.Proxy import Data.Word import Foreign.Ptr

type OffsetOf l xs = GetOffset 0 l xs

type family ByteSize x where ByteSize Word64 = 8 ByteSize Word32 = 4 ByteSize Word16 = 2 ByteSize Word8 = 1 ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>: Text " is not exportable.")

type family GetOffset n (l :: Symbol) xs where GetOffset n l ( '(l,a) ': xs) = '(n,a) GetOffset n l ( '(x,a) : xs) = GetOffset (n+ByteSize a) l xs GetOffset n l '[] = TypeError (Text "Missing field: " :<>:

ShowType l)

newtype Struct (a :: [(Symbol,*)]) = Struct (Ptr ())

get :: forall l fs n a. (OffsetOf l fs ~ '(n,a), KnownNat n) => Struct fs -> Proxy l -> Ptr a get (Struct p) _ = plusPtr p (fromInteger (natVal (Proxy :: Proxy n)))

type MyStruct = [ '("A",Word8), '("B",Word8), '("C",Int) ]

testOk :: Struct MyStruct -> Ptr Word8 testOk s = get s (Proxy :: Proxy "B")

{- testNotOk :: Struct MyStruct -> Ptr Word8 testNotOk s = get s (Proxy :: Proxy "X") --}

{- type MyOtherStruct = [ '("A",Int), '("B",Word8) ]

testNotOk :: Struct MyOtherStruct -> Ptr Word8 testNotOk s = get s (Proxy :: Proxy "B") --}

On Mon, Nov 16, 2015 at 1:21 PM, Ben Gamari mailto:ben@smart-cactus.org> wrote:

While preparing some additional documentation for Iavor's custom type errors work (which has been merged; thanks Iavor!) I noticed that Dominique Devriese has raised some additional questions on the proposal [1].

In particular, Dominique suggests that perhaps TypeError should simply be of kind `ErrorMessage -> Constraint`. My understanding of the proposal is that the intention is that `TypeError`s should be usable on the RHS of type functions, like `error` on the term level. However, is this strictly necessary? Is there any place where you couldn't just as easily express the `TypeError` as a constraint?

If not, it seems like this may be substantially simpler approach and totally side-steps the detection of `TypeError` in inappropriate places on the RHS.

Regardless, it seems like this (and the other questions) is worth addressing in the proposal.

Cheers,

- Ben

[1] https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors#Somedesignqu...:

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs