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 <[email protected]>: > 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 <[email protected] >> <mailto:[email protected]>> 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 >> [email protected] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > > > > _______________________________________________ > ghc-devs mailing list > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
