Further custom type error questions

[Iavor Diatchki]

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 <ben at 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#SomedesignquestionsDominiqueDevriese
> :
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151116/d573bd5c/attachment.html>