PROPOSAL: Make Data.Type.Bool.If polykinded

[Richard Eisenberg]

Hi Merijn,

I believe that `If` is already the way you want:

  λ> :k If
  If :: Bool -> k -> k -> k

The problem in your code is that GHC is a little... er... unprincipled about the kind of `()`. It basically assumes that `()` is of kind `*` unless it is very, absolutely, abundantly obvious that it should have kind `Constraint`. Your code is not abundantly obvious enough in this regard. If you say `If cond (() :: Constraint) (...) => ...`, I believe your code will work.

Does this in fact work for you?

Richard

On Sep 1, 2014, at 11:41 PM, Merijn Verstraaten <merijn at inconsistent.nl> wrote:

> Ola!
> 
> Currently we have:
> 
> type family If cond tru fls where
>    If True tru fls = tru
>    If False tru fls = fls
> 
> Unfortunately, this appears to turned into a monomorphicly kinded type family by GHC, which means it’s impossible to do
> 
> foo :: If cond () (“Condition does not hold” ~ “”) => Foo -> Bar
> 
> or similar fancy constraints.
> 
> I hereby propose altering If to:
> 
> type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where
>   If True tru fls = tru
>   If False tru fls = fls
> 
> Allowing it to work with kinds other than *.
> 
> Discussion period: 2 weeks? Seems like a minor change.
> 
> Cheers,
> Merijn
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries