Pattern synonyms: help needed: capturing EvBinds in tcPat

[Dr. ERDI Gergo]

Hi,

Based on feedback from Simon PJ a couple weeks ago, I started a 
substantial rewrite of the typecheker of pattern synonyms, to support 
existential types. My latest code (full of 'stash' commits and a huge 
amount of 'traceTc' calls) is available in the pattern-synonyms-wip branch 
of http://github.com/gergoerdi/ghc.git.

What I'm struggling with, is capturing the evidence bindings during the
typechecking of a pattern which is a pattern synonym occurance. For 
example, suppose I have the following module:

{-# LANGUAGE GADTs, PatternSynonyms #-}
module ConstrEx where

data T where
     MkT :: (Eq b) => b -> b -> T

pattern P b b' = (MkT b b', ())

f (P x y) = [x] == [y]


The names in the following will refer to the output of 
pattern-synonyms-wip with --ddump-tc-trace.

The right-hand side of 'f' requires an instance Eq [b], and is given an 
instance $dEq_an5 :: Eq b, so it binds a dictionary '$dEq_an7 = 
GHC.Classes.$fEq[] @[b] [$dEq_an5]'. This makes sense. However, inside 
'tcPatSynPat', which is the version of 'tcPat' for pattern synonym 
occurances, the 'checkConstraints'-wrapped  call to (eventually) 
'thing_inside' doesn't capture this binding (I get back an empty 
'TcEvBinds').

This causes problems further on because even though $dEq_an5 is going to 
be in scope while generating code for the right-hand side (since 
'tcInstPatSyn', the function that instantiates 'P x y' into '(MkT x y, ())', 
substitutes the name of the dictionary bound by MkT, $dEq_amS, to 
$dEq_an5), but $dEq_an7 is not, since its binding is not emitted by 
'tcPatSynPat' (since it doesn't get it from 'checkConstraints'). Looking 
at the tc-trace log, I see '$dEq_an7 = GHC.Classes.$fEq[] @[b] [$dEq_an5]' 
on line 2070, way after the call to 'checkConstraints' returns on line 
1811.

I realize the above description is basically incomprehensible unless you 
go through the trouble of reading through 'tcPatSynDecl', 'tcPatSynPat' 
and 'tcInstPatSyn', but I don't yet know how to even formulate my question 
more succinctly.

Any help is appreciated.

Thanks,
 	Gergo

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
GDK is the GNU Not Unix Image Manipulation Program Tool Kit Drawing Kit