<div dir="ltr">Hello,<div><br></div><div>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. </div><div><br></div><div>-Iavor</div><div>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.</div><div><br></div><div><br></div><div><div><font face="monospace, monospace">{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, DataKinds #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE ScopedTypeVariables #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">import GHC.TypeLits</font></div><div><font face="monospace, monospace">import Data.Proxy</font></div><div><font face="monospace, monospace">import Data.Word</font></div><div><font face="monospace, monospace">import Foreign.Ptr</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">type OffsetOf l xs = GetOffset 0 l xs</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">type family ByteSize x where</font></div><div><font face="monospace, monospace"> ByteSize Word64 = 8</font></div><div><font face="monospace, monospace"> ByteSize Word32 = 4</font></div><div><font face="monospace, monospace"> ByteSize Word16 = 2</font></div><div><font face="monospace, monospace"> ByteSize Word8 = 1</font></div><div><font face="monospace, monospace"> ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:</font></div><div><font face="monospace, monospace"> Text " is not exportable.")</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">type family GetOffset n (l :: Symbol) xs where</font></div><div><font face="monospace, monospace"> GetOffset n l ( '(l,a) ': xs) = '(n,a)</font></div><div><font face="monospace, monospace"> GetOffset n l ( '(x,a) : xs) = GetOffset (n+ByteSize a) l xs</font></div><div><font face="monospace, monospace"> GetOffset n l '[] = TypeError (Text "Missing field: " :<>:</font></div><div><font face="monospace, monospace"> ShowType l)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">newtype Struct (a :: [(Symbol,*)]) = Struct (Ptr ())</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">get :: forall l fs n a.</font></div><div><font face="monospace, monospace"> (OffsetOf l fs ~ '(n,a), KnownNat n) =></font></div><div><font face="monospace, monospace"> Struct fs -></font></div><div><font face="monospace, monospace"> Proxy l -></font></div><div><font face="monospace, monospace"> Ptr a</font></div><div><font face="monospace, monospace">get (Struct p) _ = plusPtr p (fromInteger (natVal (Proxy :: Proxy n)))</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">type MyStruct = [ '("A",Word8), '("B",Word8), '("C",Int) ]</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">testOk :: Struct MyStruct -> Ptr Word8</font></div><div><font face="monospace, monospace">testOk s = get s (Proxy :: Proxy "B")</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">{-</font></div><div><font face="monospace, monospace">testNotOk :: Struct MyStruct -> Ptr Word8</font></div><div><font face="monospace, monospace">testNotOk s = get s (Proxy :: Proxy "X")</font></div><div><font face="monospace, monospace">--}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">{-</font></div><div><font face="monospace, monospace">type MyOtherStruct = [ '("A",Int), '("B",Word8) ]</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">testNotOk :: Struct MyOtherStruct -> Ptr Word8</font></div><div><font face="monospace, monospace">testNotOk s = get s (Proxy :: Proxy "B")</font></div><div><font face="monospace, monospace">--}</font></div></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 16, 2015 at 1:21 PM, Ben Gamari <span dir="ltr"><<a href="mailto:ben@smart-cactus.org" target="_blank">ben@smart-cactus.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
While preparing some additional documentation for Iavor's custom type<br>
errors work (which has been merged; thanks Iavor!) I noticed that<br>
Dominique Devriese has raised some additional questions on the proposal<br>
[1].<br>
<br>
In particular, Dominique suggests that perhaps TypeError should simply<br>
be of kind `ErrorMessage -> Constraint`. My understanding of the<br>
proposal is that the intention is that `TypeError`s should be usable on<br>
the RHS of type functions, like `error` on the term level. However, is<br>
this strictly necessary? Is there any place where you couldn't just as<br>
easily express the `TypeError` as a constraint?<br>
<br>
If not, it seems like this may be substantially simpler approach and<br>
totally side-steps the detection of `TypeError` in inappropriate places<br>
on the RHS.<br>
<br>
Regardless, it seems like this (and the other questions) is worth<br>
addressing in the proposal.<br>
<br>
Cheers,<br>
<br>
- Ben<br>
<br>
<br>
[1] <a href="https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors#SomedesignquestionsDominiqueDevriese" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors#SomedesignquestionsDominiqueDevriese</a>:<br>
</blockquote></div><br></div>