Changes between Initial Version and Version 1 of ClassMethodTypes/TypedTrans


Ignore:
Timestamp:
Feb 2, 2006 2:36:45 AM (10 years ago)
Author:
chak@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ClassMethodTypes/TypedTrans

    v1 v1  
     1The problem with a typed preserving translation in the presence of functional dependencies is illustrated by Martin Sulzmann's ''critical example'':
     2{{{
     3class C a b | a -> b
     4instance C Int Bool
     5
     6class D a where
     7  foo :: C a b => a -> b
     8instance D Int where
     9  foo _ = False
     10}}}
     11The straight forward translation is as follows:
     12{{{
     13data C a b = MkC
     14dC_Int_Bool = MkC
     15
     16data D a = MkD {foo :: forall b. C a b -> a -> b}
     17dD_Int = MkD {foo = \_ -> False}
     18}}}
     19The translated program is not type correct (as `b` is universally quantified in `foo`s signature).  In the source, however, the functional dependency instantiates `b` to `Bool` in the `D Int` instance.
     20
     21GHC currently circumvents the problem by rejecting the source program.