[Haskell-cafe] Type level sets with GADTs, fundeps etc

[J.Burton at brighton.ac.uk]

At Tue, 15 Jul 2008 10:02:23 -0400,
Jeff Polakow wrote:
[...]
> >
> Type classes are open so there is nothing to prevent you from adding another
> instance for If, perhaps in a different module, which returns some arbitrary
> type.

I see what you mean...so I tried to make Ins return an LSet of
"something", like this:

data LSet t where
    Nil :: LSet Nil
    Ins :: (Member a t b
          , If b t (a ::: t) r) 
          => L a -> LSet t -> LSet r

/home/jim/sdf-bzr/dsel/TF/Set-July08.hs:44:9:
    No instance for (If b t (a ::: t) r)
      arising from a use of `Ins'
                   at /home/jim/sdf-bzr/dsel/TF/Set-July08.hs:44:9-11
    Possible fix: add an instance declaration for (If b t (a ::: t) r)
    In the expression: Ins
    In the definition of `insert': insert = Ins

/home/jim/sdf-bzr/dsel/TF/Set-July08.hs:68:6:
    Inferred type is less polymorphic than expected
      Quantified type variable `a' is mentioned in the environment:
        insert :: L a -> LSet t -> LSet r
          (bound at /home/jim/sdf-bzr/dsel/TF/Set-July08.hs:44:0)
    When checking an existential match that binds
        t :: L a
    The pattern(s) have type(s): LBox
    The body has type: LSetBox
    In a case alternative: LBox t -> LSetBox (insert t s)
    In the expression:
        case fromChar c of LBox t -> LSetBox (insert t s)
Failed, modules loaded: none.

> 
> -Jeff
> 
> 
> ---
> 
> This e-mail may contain confidential and/or privileged information. If you
> are not the intended recipient (or have received this e-mail in error)
> please notify the sender immediately and destroy this e-mail. Any
> unauthorized copying, disclosure or distribution of the material in this
> e-mail is strictly forbidden.
> [2  <text/html; US-ASCII (7bit)>]
>