Ed Komp replied to Simon Peyton-Jones: > Within the GHC compiler > > can't be instantiated to Double --- but that's tricky to pin down. > this may be tricky to pin down. > But, there is specific information in my example to exclude Double: > I had carefully constructed the type definitions to avoid > ambiguity.
Indeed, the open world assumption makes it rather difficult to define a constraint that two type variables must denote different types. I wish it were possible to easily write forall a b. (NotEq a b) => ... Functional dependencies can be used to achieve a similar effect -- but sometimes that are not applicable. I wish there were a way to assert to the compiler that there will be no more instances of a specific class. The compiler can record this assumption in the object file. When the compiler builds the final executable and finds an unexpected instance, the compiler can tell the user that he lied. > | class SubType a b where > | inj :: a -> b > | prj :: b -> Maybe a > | > | instance SubType a (Either a x) where > | inj =3D Left > | prj =3D either Just (const Nothing) > | > | instance (SubType a b) =3D> SubType a (Either x b) where > | inj =3D Right . inj > | prj =3D either (const Nothing) prj > | > | type BaseType = Either Integer ( Either Bool () ) > | > | type Value = (Either Double BaseType) > | > | data Foo = forall x. (SubType x BaseType) => MkFoo x > | > | test :: Foo -> Value > | test (MkFoo x) = inj x I'm quite dubious that test can be typed at all (see below). Even if the problem with overlapping instances could be solved. I seem to remember being on this road before. I'd be great to get GHC to run the typechecker at run time, to choose the right instance. Alas. In the example above, the constraint on Foo only guarantees (SubType x BaseType). When we create MkFoo True, for example, the compiler knows the type the value being encapsulated, chooses the right instance (that is, the dictionary), and places the dictionary and the value into the MkFoo envelope. The function test executes "inj x" whose return type is different from the BaseType. that is, 'inj' implicitly has the constraint (SubType x Value). However, MkFoo x only guarantees (SubType x BaseType). This is not a technicality. Let us disambiguate the instances and remove all overlapping: > class SubType a b where > inj :: a -> b > prj :: b -> Maybe a > instance SubType Bool (Either Bool x) where > inj = Left > prj = either Just (const Nothing) > instance SubType Integer (Either Integer x) where > inj = Left > prj = either Just (const Nothing) > instance (SubType Bool b) => SubType Bool (Either Integer b) where > inj = Right . inj > prj = either (const Nothing) prj > instance (SubType Bool b) => SubType Bool (Either Double b) where > inj = Right . inj > prj = either (const Nothing) prj > instance (SubType Integer b) => SubType Integer (Either Double b) where > inj = Right . inj > prj = either (const Nothing) prj > type BaseType = Either Integer ( Either Bool () ) > type Value = (Either Double BaseType) > data Foo = forall x. (SubType x BaseType) => MkFoo x > -- test :: Foo -> Value > -- test (MkFoo x) = inj x > test1 :: Foo -> BaseType > test1 (MkFoo x) = inj x This code types and even runs: *> test1 $ MkFoo True *> Right (Left True) Indeed, when the compiler sees MkFoo True, it chooses the right instance of the class (SubType x BaseType), and packs the corresponding dictionary into MkFoo. When we run test1 $ MkFoo True, the compiler extracts the dictionary from MkFoo, extracts the field inj from that dictionary, and runs the corresponding procedure. At this time (at run time), the compiler does not and cannot choose instances. If we uncomment the procedure test above, we predictably get the error: /tmp/k2.hs:32: Could not deduce (SubType x Value) from the context (SubType x BaseType) Probable fix: Add (SubType x Value) to the existential context of a data constructor Or add an instance declaration for (SubType x Value) arising from use of `inj' at /tmp/k2.hs:32 In the definition of `test': inj x As we saw above, we cannot widen the constraint at the run time. The function test wants to use a different function inj -- not the one associated with (SubType Bool BaseType) -- the chosen instance -- but a different one, associated with an instance (SubType Bool Value). However, we cannot chose the instance at that time because the compiler does not know the exact type of the value in the existential envelope. To do as you wish, the compiler would have had to compile the typechhecer into the target executable code. Not that it would be a bad idea. _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell