How does the ambiguity check work

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

How does the ambiguity check work

Jan van Brügge
Hi lovely people,

I am currently trying to wrap my head around the ambiguity check in GHC.
In particular for those two instances:

```

class RowEquality where
    rowEqual :: Bool

instance (1 ~ 2) => RowEquality where
    rowEqual = True

instance ( ("foo" ::: Int & RNil) ~ ("bar" ::: String & "foo" ::: Int &
RNil) ) => RowEquality where
    rowEqual = True
```

I would expect them to behave the same but the second one throws an
error when trying to compile the module (*before* using `rowEqual` -
that would obviously throw a type error in both cases):

```
Test.hs:24:10: error:
    • Could not deduce: (| "foo" :: Int |)
                        ~ (| "bar" :: [Char], "foo" :: Int |)
      from the context: (("foo" ::: Int) & RNil)
                        ~ (("bar" ::: String) & (("foo" ::: Int) & RNil))
        bound by an instance declaration:
                   ((("foo" ::: Int) & RNil)
                    ~ (("bar" ::: String) & (("foo" ::: Int) & RNil))) =>
                   RowEquality
        at Test.hs:24:10-94
    • In the ambiguity check for an instance declaration
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the instance declaration for 'RowEquality
```

I have troubles to understand why GHC tries to solve the constraint
there. I worked through `checkAmbiguity` in `TcValidity` and the
function it calls, but from what I can see is that it also tries to
solve the `(1 ~ 2)` and fails in the same way as with the second one. I
cannot find any reason why the two are treated differently.

Thank you
Jan

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: How does the ambiguity check work

Richard Eisenberg-5
Hi Jan,

The ambiguity check has a simple description. To test if a type `ty` is ambiguous, do this:

```
x :: ty
x = x
```

Iff that type-checks, the type is unambiguous. That's it!

The check does not manufacture a binding `x`, but the implementation runs through the type-checking process for a binding just like the one I've written here.

In your case, I have two hypotheses:
1. Presumably, you have a solver plugin at work. That may explain the difference in behavior between the two cases.
2. There may be kind variables at work, and these may end up ambiguous. It's definitely worth trying with -fprint-explicit-kinds.

I hope this helps!
Richard
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: How does the ambiguity check work

Nicolas Frisby
IIUC Jan is working on a ghc branch, not a plugin. But perhaps this ticket will point in the right direction anyway? HTH.


On Mon, Sep 30, 2019, 01:44 Richard Eisenberg <[hidden email]> wrote:
Hi Jan,

The ambiguity check has a simple description. To test if a type `ty` is ambiguous, do this:

```
x :: ty
x = x
```

Iff that type-checks, the type is unambiguous. That's it!

The check does not manufacture a binding `x`, but the implementation runs through the type-checking process for a binding just like the one I've written here.

In your case, I have two hypotheses:
1. Presumably, you have a solver plugin at work. That may explain the difference in behavior between the two cases.
2. There may be kind variables at work, and these may end up ambiguous. It's definitely worth trying with -fprint-explicit-kinds.

I hope this helps!
Richard
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs