Question about ambiguous predicates in pattern bindings

[Benjamin Redelings]

Hi,

1. I'm reading "A Static semantics for Haskell" and trying to code it 
up.  I came across some odd behavior with pattern bindings, and I was 
wondering if someone could explain or point me in the right direction.

Suppose you have the declaration

     (x,y) = ('a',2)

My current code is yielding:

     x :: Num a => Char

     y :: Num a => a

However, I notice that ghci gives x the type Char, with no constraint, 
which is what I would expect.  It also gives y the type 'Num b => b', so 
I don't think it is defaulting a to Int here.

The weird results from my code stem from rule BIND-PRED in Figure 15 of 
https://homepages.inf.ed.ac.uk/wadler/papers/staticsemantics/static-semantics.ps

     E  |-  bind ~~> \dicts : theta -> monobinds in bind : (LIE_{encl}, 
theta => LVE)

Here theta = ( Num a ) and LVE = { x :: Char, y :: a }.  So, theta => LVE is

     { x :: Num a => Char, y :: Num a => a }

The obvious thing to do is avoid changing a type T to Num a => T if T 
does not contain a.  Also I'm not totally sure if that trick gets to the 
bottom of the issue.  However, the paper doesn't mention define theta => 
LVE that way.  Is there something else I should read on this?

2. If we just chop out predicates which mention variables not in the 
type ( == ambiguous predicates?) then I'm not totally sure how to create 
code for this.

I would imagine that we have something like

     tup dn = ('a', fromInteger dn 2)

     x = case (tup dn) of (x,y) -> x

     y dn case (tup dn) of (x,y) -> y

In this case its not clear where to get the `dn` argument of `tup` from, 
in the definition of `x`.  Can we pass in `undefined`?  Should we do 
something else?

If anyone can shed light on this, I would be grateful :-)

-BenRI