[Haskell-cafe] Re: checking types with type families

[Claus Reinke]

>>   class C a b | a->b where
>>     op :: a -> b
> 
>>   instance C Int Bool where
>>     op n = n>0
> 
>>   data T a where
>>     T1 :: T a
>>     T2 :: T Int
> 
>>   -- Does this typecheck?
>>   f :: C a b => T a -> Bool
>>   f T1 = True
>>   f T2 = op 3
> 
>> The function f "should" typecheck because inside the T2 branch we know
>> that (a~Int), and hence by the fundep (b~Bool).  

Perhaps I'm confused, but there seems to be no link between
the call 'op 3' and 'a' in this example. While the 'desugaring' 
introduces just such a connection.

>> g :: C a b => TT a -> Bool
>> g TT1 = True
>> g (TT2 eq) = op (if False then cast eq undefined else 3)

If we add that connection to the original example, it typechecks
as well:

f :: forall a b. C a b => T a -> Bool
f T1 = True
f T2 = op (3::a)

We could also write:

f :: forall a b. C a b => T a -> Bool
f T1 = True
f T2 = (op :: a -> Bool) 3

Though there is a long-standing issue that we cannot write

f :: forall a b. C a b => T a -> Bool
f T1 = True
f T2 = (op :: a -> b) 3

as that results in the counter-intuitive

    Couldn't match expected type `Bool' against inferred type `b'
      `b' is a rigid type variable bound by
          the type signature for `f'
            at C:\Users\claus\Desktop\tmp\fd-local.hs:17:14
    In the expression: (op :: a -> b) 3
    In the definition of `f': f T2 = (op :: a -> b) 3

Which seems to be a variant of Oleg's example? I thought there 
was a ticket for this already, but I can't find it at the moment. It
would be useful to have standard keywords (FD, TF, ..) to make
ticket querying for common topics easier, and to record the 
status of FD vs TF in trac.

There used to be a difference the other way round as well
(more improvement with FDs than with TFs), which I found
while searching trac for the other issue:

http://hackage.haskell.org/trac/ghc/ticket/2239

>From testing that example again with 6.12.3, it seems that
bug has since been fixed but the ticket not closed?

>> But we have no formal type system for fundeps that describes this, 
>> and GHC's implementation certainly rejects it. 

I've not yet finished Martin's paper, and your recent major work 
is also still on my reading heap, but just to get an idea of the 
issues involved: from CHR-based fundep semantics, the step 
to local reasoning would seem to encounter hurdles mainly in 
the interaction of local and non-local reasoning, right?

If we only wanted to add local reasoning, the standard solution
would be to make copies, so that the local steps don't affect the
global constraint store (somewhat more practical, we could add
tags to distinguish local and global stores; for sequential 
implementations, Prolog-style variable trails could probably be 
extended to account for constraints as well).

But we want local reasoning to make use of non-local constraints 
and variable bindings, and we probably want to filter some, but
not all, local reasoning results back into the global store.

Are these the issues, or are there others?

Claus