[Haskell-cafe] RE: Instances That Ignore Type Constraints? (HList-related)

[Ralf Lammel]

Yeah, I was also thinking of impredicative types and that they would
make this problem go away. First of all, we may need to wait a while for
such types to become available in Haskell, but Daan has good stuff at
avail.

Also, for clarity, let me just point out that this is really about an
*interaction* of impredicativeness *and* type classes. Hence, I really
think that an argument in favor of impredicative types is slightly
overrated unless a Haskell approach to impredicativeness is fully
conclusive for the type-class story. The following queries make it
clear:

Prelude> null [fromEnum]

<interactive>:1:6:
    Ambiguous type variable `a' in the constraint:
      `Enum a' arising from use of `fromEnum' at <interactive>:1:6-13
    Probable fix: add a type signature that fixes these type variable(s)

Prelude> null [id]
False

More importantly, I need more input to fully endorse the appropriateness
of impredicative types in this sort of context. That is, the question is
... what does it *mean* to wrap (or to box or to cartoon) an expression
with non-escaping type variables that locally occur in type-class
constraints?

GHC/Haskell, as of today:
- it means nothing; type error.

Some sort of impredicative type:
- it means universal quantification

Potentially elsewhere:
- it means existential quantification

In Ghc with incoherent instances:
- see above; except that the instance is actually selected.

In addition to this scary diversity, all the three last choices are
bogus in some sense because the quantified variables are totally
inaccessible; so why would a type system honor such potentially
accidental opaqueness. In summary, this makes me conclude that null
[fromEnum] is just a really loose question to ask, which is perhaps just
better rejected by a strong type system, no? Please, prove that I am
wrong. :-)

Ralf


Oleg wrote:

> When GHC does implement
> MLF and start explicitly supporting impredicative types, the problem
> would be fixed indeed... Currently, the only way to achieve the same
> effect is to do this manually:
> 
> 	newtype W = W (forall a. (Enum a) => a -> Int)
> 
> *Main> null [W fromEnum]
> False
> 
> 	Perhaps indeed we should move to Cafe...