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