Opened 2 years ago

Closed 22 months ago

#7786 closed bug (fixed)

strange errors when deducing constraints

Reported by: heisenbug Owned by: simonpj
Priority: normal Milestone: 7.8.1
Component: Compiler Version: 7.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_fail/T7786
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

Please load attached file in ghci and observe the resulting error message. I have added my commentaries inline to what appears fishy to me. All may technically be ok, but look quite confusing.

[1 of 1] Compiling Main             ( pr7786.hs, interpreted )

pr7786.hs:74:22:
    Couldn't match type `Intersect
                           [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv'
                  with 'Empty [KeySegment]
    Inaccessible code in
      a pattern with constructor
        Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
      in a pattern binding in
           'do' block

Yes, ok, (Nil :: Sing Empty) does not unify with (forall xxx. Nil :: Sing xxx).

    Relevant bindings include
      addSub :: Database inv
                -> Sing [KeySegment] k
                -> Database sub
                -> Maybe (Database (BuriedUnder sub k inv))
        (bound at pr7786.hs:74:1)
      db :: Database inv (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k (bound at pr7786.hs:74:11)
      sub :: Database sub (bound at pr7786.hs:74:13)
    In the pattern: Nil
    In the pattern: Nil :: Sing xxx
    In a stmt of a 'do' block:
      Nil :: Sing xxx <- return
                           (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)

pr7786.hs:78:31:
    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])

This one is highly disturbing. I think the user should never see such a message. Scary. This is the reason for the ticket.

      bound by a pattern with constructor
                 Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
               in a pattern binding in
                    'do' block
      at pr7786.hs:74:22-24
    Relevant bindings include
      addSub :: Database inv
                -> Sing [KeySegment] k
                -> Database sub
                -> Maybe (Database (BuriedUnder sub k inv))
        (bound at pr7786.hs:74:1)
      db :: Database inv (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k (bound at pr7786.hs:74:11)
      sub :: Database sub (bound at pr7786.hs:74:13)
    In the second argument of `($)', namely `Sub db k sub'
    In a stmt of a 'do' block: return $ Sub db k sub
    In the expression:
      do { Nil :: Sing xxx <- return
                                (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
           return $ Sub db k sub }
Failed, modules loaded: none.

Now comment line 74 and uncomment l. 75 and reload:

pr7786.hs:75:22:
    Couldn't match type `Intersect
                           [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv'
                  with `Intersect
                          [KeySegment] (BuriedUnder sub1 k1 ('Empty [KeySegment])) inv1'

Hmm, I vaguely understand why those new degrees of freedom arise.

    NB: `Intersect' is a type function, and may not be injective

Probably irrelevant, no need to backwards guess here, as we have -XScopedTypeVariables turned on.

    The type variables `sub', `k', `inv' are ambiguous
    Expected type: Sing
                     (Inventory [KeySegment])
                     (Intersect
                        [KeySegment] (BuriedUnder sub1 k1 ('Empty [KeySegment])) inv1)
      Actual type: Sing
                     (Inventory [KeySegment])
                     (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv)
    Relevant bindings include
      addSub :: Database inv1
                -> Sing [KeySegment] k1
                -> Database sub1
                -> Maybe (Database (BuriedUnder sub1 k1 inv1))
        (bound at pr7786.hs:74:1)
      db :: Database inv1 (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k1 (bound at pr7786.hs:74:11)
      sub :: Database sub1 (bound at pr7786.hs:74:13)
    In the pattern:
      Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv)
    In a stmt of a 'do' block:
      Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return
                                                                     (buryUnder (dbKeys sub) k Nil
                                                                      `intersectPaths` dbKeys db)
    In the expression:
      do { Nil :: Sing ((sub `BuriedUnder` k) Empty
                        `Intersect` inv) <- return
                                              (buryUnder (dbKeys sub) k Nil
                                               `intersectPaths` dbKeys db);
           return $ Sub db k sub }
Failed, modules loaded: none.

Now comment line 75 and uncomment l. 76 and reload:

[1 of 1] Compiling Main             ( pr7786.hs, interpreted )


pr7786.hs:76:51:
    Couldn't match type `Intersect
                           [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv'
                  with 'Empty [KeySegment]
    Expected type: Sing (Inventory [KeySegment]) ('Empty [KeySegment])
      Actual type: Sing
                     (Inventory [KeySegment])
                     (Intersect
                        [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv)

Err... But (Nil :: Sing Empty) is exactly the annotation on the Nil constructor in the GADT definition!

    Relevant bindings include
      addSub :: Database inv
                -> Sing [KeySegment] k
                -> Database sub
                -> Maybe (Database (BuriedUnder sub k inv))
        (bound at pr7786.hs:74:1)
      db :: Database inv (bound at pr7786.hs:74:8)
      k :: Sing [KeySegment] k (bound at pr7786.hs:74:11)
      sub :: Database sub (bound at pr7786.hs:74:13)
    In the first argument of `return', namely
      `(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)'
    In a stmt of a 'do' block:
      Nil :: Sing Empty <- return
                             (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
    In the expression:
      do { Nil :: Sing Empty <- return
                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
           return $ Sub db k sub }
Failed, modules loaded: none.

Now comment line 76 and uncomment l. 77 and reload:

All is dandy!

Attachments (1)

pr7786.hs (3.4 KB) - added by heisenbug 2 years ago.
reproduction testcase

Download all attachments as: .zip

Change History (6)

Changed 2 years ago by heisenbug

reproduction testcase

comment:1 Changed 2 years ago by simonpj

  • difficulty set to Unknown
  • Owner set to simonpj

I took a look. I think I know how to improve. More after the ICFP deadline

comment:2 Changed 2 years ago by igloo

  • Milestone set to 7.8.1

comment:3 Changed 2 years ago by simonpj@…

commit 6ebab3df7e68f8325ef60111c0c7755dd6ffcc91

Author: Simon Peyton Jones <[email protected]>
Date:   Mon Apr 22 12:50:24 2013 +0100

    Never unify a SigTyVar with a non-tyvar type (fixes Trac #7786)
    
    This unwanted unification was happening in the zonking phase
    which un-flattens type-function applications (TcMType.zonkFlats,
    try_zonk_fun_eq).  The main unifier is careful to make the check,
    but I'd forgotten it here.  That in turn led to a very confusing
    error message.

 compiler/typecheck/TcMType.lhs |    4 ++--
 1 files changed, 2 insertions(+), 2 deletions(-)

comment:4 Changed 2 years ago by simonpj

  • Test Case set to indexed-types/should_fail/T7786

Thanks for reporting this! Now fixed.

Simon

comment:5 Changed 22 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
Note: See TracTickets for help on using tickets.