[Haskell-cafe] Question about ambiguity and defaulting in recursive bindings

[Benjamin Redelings]

1. Hmm... Perhaps ghc changes the code to

fgtuple:: (Eq a, Num a) => (Char -> a -> Char, Char -> Char -> Char)
fgtuple dEq dNum =
    let f c i   = if i == 10 then c else g c 'b'
        g 'a' w = f 'b' 10
        g z   w = z
    in (f,g)

f :: forall a. (Eq a, Num) => Char -> a -> Char
f dEq dNum = case fgtuple dEq dNum of (f,g) -> f

g :: Char -> Char -> Char
g = case fgtuple dEqInt dNumInt (f,g) -> g

In order words,

* the definition of fgtuple is not ambiguous.

* the defaulting is applied only to the definition of g, not the 
definition of fgtuple.

Does that sound right?

2. Running ghc -ddump-tc shows:

   {Exports: [f <= f_a2gf
                wrap: <>,
              g <= g_a2gi
                wrap: <> @ Integer $dEq_a2xJ $dNum_a2xK]

The "wrap" code looks like the extra arguments that are applied by 
defaulting.

-BenRI

On 1/19/22 11:19 AM, Benjamin Redelings wrote:

> Hi,
>
> I am trying to understand how GHC treats the following declaration.
>
> f c i   = if i == 10 then c else g c 'b'
> g 'a' w = f 'b' 10
> g z   w = z
>
> l = (f 'a' (1::Int), f 'a' (1.0::Double))
>
> It seems to me like, after defaulting, f should have the following type:
>
>      Char -> Int -> Char
>
> However, looking at -ddump-tc, GHC is deriving the polymorphic type
>
>      forall a. (Eq a, Num a) => Char -> a -> Char
>
> That's much nicer, because its more flexible.  But I'm confused, 
> because it looks like GHC is defaulting 'g', but not 'f', even though 
> they are in the same recursive group.  This seems to contradict 
> "Typing Haskell in Haskell", which is what I am looking at right now.  
> If that is correct, can anybody point me to a paper or documentation 
> about how this works?
>
> More detail:
>
> 1. If I understand correctly, the definitions of `f` and `g` are 
> mutually recursive, and should be typed together, and the declaration 
> group is not restricted.
>
> 2. It seems like, before generalization, we have
>
>      f :: Char -> a -> Char
>      g :: Char -> Char -> Char
>      Predicates include (Eq a, Num a)
>
> 3. Looking at the paper "Typing Haskell in Haskell" (THIH), it looks 
> like the predicates (Num a, Eq a) should cause an ambiguity in the 
> definition of g:
>
> * a is present in the definition of f, but not the definition of g
>
> * so the type (Eq a, Num a) => Char -> Char -> Char is ambiguous.
>
> * more generally, it seems like THIH treats any predicates with a type 
> variable that is part of some, but not all, types in the declaration 
> group to be ambiguous.  Does this sound right?
>
> 4. Then, again following THIH, this ambiguous predicate should be 
> defaulted to Int.
>
> I THINK this should lead to
>
> 	f :: Char -> Int -> Char
> 	g :: Char -> Char -> Char
>
> 5. However, I'm still not sure I'm understanding this right, because a 
> few things still don't make sense:
>
> * First, THIH seems to eliminate the defaulted predicates without 
> substituting a -> Int.  But the type for f DOES mention `a`, so how 
> can we avoid substituting?
>
> * Second, GHC accepts the code with no warnings or errors. There is 
> some kind of defaulting going on, because GHC rejects the code if I 
> add "default ()". Is there some way for GHC to default only g, but not f?
>
> I wonder if this involves a difference between Haskell '98 and Haskell 
> 2010?
>
> I also wonder how much I should rely on THIH?  Maybe the language has 
> moved on since then?
>
> -BenRI
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220119/7e71e1e3/attachment.html>