So perhaps you can update the wiki page to give an example like this, and thereby explain the design choice?  Or have a FAQ: “why not give TypeErorr the kind String -> Constraint?”.

The thought will be lost in email!

Simon

From: Iavor Diatchki [mailto:iavor.diatchki@gmail.com]
Sent: 17 November 2015 00:10
To: Ben Gamari
Cc: Simon Peyton Jones; Richard Eisenberg; Dominique Devriese; ghc-devs@haskell.org
Subject: Re: Further custom type error questions

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@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: