Further custom type error questions

[Dominique Devriese]

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 <roma at ro-che.info>:
> 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
>>
>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>