Thank you very much, Ralf, for your very thorough reply. That's a very general way to deal with the issue. It never occurred to me that the "inspected" class itself might carry the availability info. Cheers, Jorge. Ralf Laemmel escreveu:

...

Given two type classes A t and B t, I'd like the typechecker to derive different A t instances depending exactly on whether t is an instance of B. In other words, is it possible to define a class (actually a type-level function) IsB t f such that:

A GHC-like type system is in principle powerful enough to do just that. We exploit such capability in HList and OOHaskell. That is, the class whose instance availability should be observed must be first set up to carry an extra functionally dependent type parameter that specifically is meant to report back on instance availability. Then, we sacrifice the capability of a generic default instance for that class to indeed report back the lack of an instance through a type-level False on the new type-parameter position, whereas all normal instances report back type-level True. The usual problem of functional-dependency violation occurs, that is, the generic default instance is not entirely standard because if it says to return False for all types, then the other instances can't claim the opposite unless we had special fundep rules for generic default instances. However, we can recover from that by making the generic default instance vacuously generic in the type-level Boolean result position so that it becomes strictly more general than any specific instance, while we still assign type-level False to the position but by a type-level cast (instead of a verbatim False).

Type-level type cast is the type-level programmer's swiss army knife.

See the illustration below.

HTH, Ralf

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-}

module M2 where

import M1

instance TypeCast x x where typeCast = id

main = do print $ b $ hasInstance ST1 print $ b $ hasInstance ST2

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-}

module M1 where

-- Type-level Booleans data T -- True data F -- False class B x where b :: x -> Bool instance B T where b = const True instance B F where b = const False

-- Sample types data ST1 = ST1 data ST2 = ST2

-- A class that reports on instance availability class B b => R x b | x -> b instance R ST1 T instance (B b, TypeCast F b) => R x b -- generically missing instance

-- Observe instance availability hasInstance :: R x b => x -> b hasInstance _ = undefined

-- The key weapon class TypeCast x y | x -> y, y -> x where typeCast :: x -> y

Jorge M. Pelizzoni ICMC - Universidade de São Paulo