constraint deduction bug?

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

constraint deduction bug?

Gabor Greif-2
In context of a bigger source file I got this error from GHC (HEAD)

    Could not deduce (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty
[KeySegment])) inv
                      ~ 'Empty [KeySegment])
    from the context (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty
[KeySegment])) inv
                      ~ 'Empty [KeySegment])
      bound by a pattern with constructor
                 Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
               in a pattern binding in
                    'do' block

Can somebody confirm that this constraint should be trivially deducible from
the context?

Then I'll try to come up with a reduced repro case.

Cheers,

        Gabor


Reply | Threaded
Open this post in threaded view
|

constraint deduction bug?

Richard Eisenberg-2
It certainly looks trivial to me.

Richard

On Mar 21, 2013, at 7:59 PM, Gabor Greif <ggreif at gmail.com> wrote:

> In context of a bigger source file I got this error from GHC (HEAD)
>
>    Could not deduce (Intersect
>                        [KeySegment] (BuriedUnder sub k ('Empty
> [KeySegment])) inv
>                      ~ 'Empty [KeySegment])
>    from the context (Intersect
>                        [KeySegment] (BuriedUnder sub k ('Empty
> [KeySegment])) inv
>                      ~ 'Empty [KeySegment])
>      bound by a pattern with constructor
>                 Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
>               in a pattern binding in
>                    'do' block
>
> Can somebody confirm that this constraint should be trivially deducible from
> the context?
>
> Then I'll try to come up with a reduced repro case.
>
> Cheers,
>
> Gabor
>
> _______________________________________________
> 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
|

constraint deduction bug?

Dimitrios Vytiniotis-2
Is Intersect (or some other of the constructors involved, maybe Empty?) kind-polymorphic and instantiated
in the two sites (wanted vs. given) with different kind variables which end up being unconstrained,
or something like that? Then it might be the case that we don't get a match (which is rather unintuitive, I
agree) and the constraint is not solved.

Even if it's a case like this it's probably best to do submit a small reproducible example and we will have a look.

Thanks
d-



> -----Original Message-----
> From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-
> bounces at haskell.org] On Behalf Of Richard Eisenberg
> Sent: Friday, March 22, 2013 1:11 AM
> To: Gabor Greif
> Cc: ghc-devs at haskell.org
> Subject: Re: constraint deduction bug?
>
> It certainly looks trivial to me.
>
> Richard
>
> On Mar 21, 2013, at 7:59 PM, Gabor Greif <ggreif at gmail.com> wrote:
>
> > In context of a bigger source file I got this error from GHC (HEAD)
> >
> >    Could not deduce (Intersect
> >                        [KeySegment] (BuriedUnder sub k ('Empty
> > [KeySegment])) inv
> >                      ~ 'Empty [KeySegment])
> >    from the context (Intersect
> >                        [KeySegment] (BuriedUnder sub k ('Empty
> > [KeySegment])) inv
> >                      ~ 'Empty [KeySegment])
> >      bound by a pattern with constructor
> >                 Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
> >               in a pattern binding in
> >                    'do' block
> >
> > Can somebody confirm that this constraint should be trivially
> > deducible from the context?
> >
> > Then I'll try to come up with a reduced repro case.
> >
> > Cheers,
> >
> > Gabor
> >
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
> _______________________________________________
> 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
|

constraint deduction bug?

Simon Peyton Jones
Yes, looks odd. Please do give us a test case.  Thank you!

S

| -----Original Message-----
| From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org]
| On Behalf Of Dimitrios Vytiniotis
| Sent: 22 March 2013 10:01
| To: Richard Eisenberg; Gabor Greif
| Cc: ghc-devs at haskell.org
| Subject: RE: constraint deduction bug?
|
| Is Intersect (or some other of the constructors involved, maybe Empty?)
| kind-polymorphic and instantiated in the two sites (wanted vs. given)
| with different kind variables which end up being unconstrained, or
| something like that? Then it might be the case that we don't get a match
| (which is rather unintuitive, I
| agree) and the constraint is not solved.
|
| Even if it's a case like this it's probably best to do submit a small
| reproducible example and we will have a look.
|
| Thanks
| d-
|
|
|
| > -----Original Message-----
| > From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-
| > bounces at haskell.org] On Behalf Of Richard Eisenberg
| > Sent: Friday, March 22, 2013 1:11 AM
| > To: Gabor Greif
| > Cc: ghc-devs at haskell.org
| > Subject: Re: constraint deduction bug?
| >
| > It certainly looks trivial to me.
| >
| > Richard
| >
| > On Mar 21, 2013, at 7:59 PM, Gabor Greif <ggreif at gmail.com> wrote:
| >
| > > In context of a bigger source file I got this error from GHC (HEAD)
| > >
| > >    Could not deduce (Intersect
| > >                        [KeySegment] (BuriedUnder sub k ('Empty
| > > [KeySegment])) inv
| > >                      ~ 'Empty [KeySegment])
| > >    from the context (Intersect
| > >                        [KeySegment] (BuriedUnder sub k ('Empty
| > > [KeySegment])) inv
| > >                      ~ 'Empty [KeySegment])
| > >      bound by a pattern with constructor
| > >                 Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty
| k),
| > >               in a pattern binding in
| > >                    'do' block
| > >
| > > Can somebody confirm that this constraint should be trivially
| > > deducible from the context?
| > >
| > > Then I'll try to come up with a reduced repro case.
| > >
| > > Cheers,
| > >
| > > Gabor
| > >
| > > _______________________________________________
| > > ghc-devs mailing list
| > > ghc-devs at haskell.org
| > > http://www.haskell.org/mailman/listinfo/ghc-devs
| >
| >
| > _______________________________________________
| > ghc-devs mailing list
| > ghc-devs at haskell.org
| > http://www.haskell.org/mailman/listinfo/ghc-devs
|
| _______________________________________________
| 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
|

constraint deduction bug?

Gabor Greif-2
In reply to this post by Dimitrios Vytiniotis-2
http://hackage.haskell.org/trac/ghc/ticket/7786

Thanks for responding!

Cheers,

    Gabor

On 3/22/13, Dimitrios Vytiniotis <dimitris at microsoft.com> wrote:

> Is Intersect (or some other of the constructors involved, maybe Empty?)
> kind-polymorphic and instantiated
> in the two sites (wanted vs. given) with different kind variables which end
> up being unconstrained,
> or something like that? Then it might be the case that we don't get a match
> (which is rather unintuitive, I
> agree) and the constraint is not solved.
>
> Even if it's a case like this it's probably best to do submit a small
> reproducible example and we will have a look.
>
> Thanks
> d-
>
>
>
>> -----Original Message-----
>> From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-
>> bounces at haskell.org] On Behalf Of Richard Eisenberg
>> Sent: Friday, March 22, 2013 1:11 AM
>> To: Gabor Greif
>> Cc: ghc-devs at haskell.org
>> Subject: Re: constraint deduction bug?
>>
>> It certainly looks trivial to me.
>>
>> Richard
>>
>> On Mar 21, 2013, at 7:59 PM, Gabor Greif <ggreif at gmail.com> wrote:
>>
>> > In context of a bigger source file I got this error from GHC (HEAD)
>> >
>> >    Could not deduce (Intersect
>> >                        [KeySegment] (BuriedUnder sub k ('Empty
>> > [KeySegment])) inv
>> >                      ~ 'Empty [KeySegment])
>> >    from the context (Intersect
>> >                        [KeySegment] (BuriedUnder sub k ('Empty
>> > [KeySegment])) inv
>> >                      ~ 'Empty [KeySegment])
>> >      bound by a pattern with constructor
>> >                 Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty
>> > k),
>> >               in a pattern binding in
>> >                    'do' block
>> >
>> > Can somebody confirm that this constraint should be trivially
>> > deducible from the context?
>> >
>> > Then I'll try to come up with a reduced repro case.
>> >
>> > Cheers,
>> >
>> > Gabor
>> >
>> > _______________________________________________
>> > ghc-devs mailing list
>> > ghc-devs at haskell.org
>> > http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>