Pattern synonyms: help needed: capturing EvBinds in tcPat

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

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



Reply | Threaded
Open this post in threaded view
|

Pattern synonyms: help needed: capturing EvBinds in tcPat

Richard Eisenberg-2
I took a look here and would like to help, but I'm confused: What makes you think the dictionary for (Eq [b]) would be in scope? I can see where the (Eq b) comes from (the theta that pops out of patSynSig), but where does (Eq [b]) come from?

Richard

On Sep 8, 2013, at 4:31 AM, Dr. ERDI Gergo <gergo at erdi.hu> wrote:

> 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
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs




Reply | Threaded
Open this post in threaded view
|

Pattern synonyms: help needed: capturing EvBinds in tcPat

Dr. ERDI Gergo
Hi Richard,

Thanks for looking into this!

On Mon, 9 Sep 2013, Richard Eisenberg wrote:

> I took a look here and would like to help, but I'm confused: What makes
> you think the dictionary for (Eq [b]) would be in scope? I can see where
> the (Eq b) comes from (the theta that pops out of patSynSig), but where
> does (Eq [b]) come from?

>> pattern P b b' = (MkT b b', ())
>>
>> f (P x y) = [x] == [y]

I thought when I call 'thing_inside' in tcPatSynPat, it would (eventually)
get to typechecking the right-hand side, which has a dependency on (Eq
[b]). I thought this dependency is captured somewhere around here so that
it(s solution) can be added to the pat_binds field of the ConPatOut.
Otherwise, I don't see where it should be created -- and as you can see
from the warning emitted by GHC, it is assumed later on to be there:

WARNING: file compiler/coreSyn/CoreSubst.lhs, line 272
     CoreSubst.lookupIdSubst simpleOptExpr $dEq_an7{v} [lid]
     InScope [(00, wild_00{v} [lid]), (X6, wild_X6{v} [lid]),
              (Xb, wild_Xb{v} [lid]), (amr, x{v amr} [lid]),
              (ams, y{v ams} [lid]), (amR, b{tv amR} [tv]),
              (an5, $dEq_an5{v} [lid]), (an8, cobox_an8{v} [lid]),
              (dnk, ds_dnk{v} [lid]), (dnl, ds_dnl{v} [lid]),
              (dnm, ds_dnm{v} [lid]), (dnr, cobox{v dnr} [lid]),
              (rgK, main:ConstrEx.f{v rgK} [lidx])]

here, $dEq_an5 is (Eq b), and $dEq_an7 is (Eq [b]).

So it seems the emitted core expects this (Eq [b]) to be there (bound to
the parametrised instance (Eq[] (Eq b))).

Thanks,
  Gergo