Further custom type error questions

[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 <ben at smart-cactus.org
> <mailto: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:
> 
> 
> 
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151117/281fcd28/attachment.sig>