[GHC] #9725: Constraint deduction failure

[GHC]

#9725: Constraint deduction failure
-------------------------------------+-------------------------------------
              Reporter:  heisenbug   |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
  (Type checker)                     |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:  GHC         |  Related Tickets:
  rejects valid program              |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by heisenbug):

 Replying to [comment:11 simonpj]:
 > Ah I see. You are right. But this is pretty coincidental.  If the wanted
 was `[W] ent ~ M` we'd be out of luck.  And taking account of the
 coincidence is far from straightforward; it would be a significant
 complication in the solver, which will be redundant when your stuff lands.
 >
 > So I propose to wait.  Sorry Gabor, but Richard's stuff is itself a
 major increment, and I just don't know what a simple cut-down version
 might look like.  ETA is up to Richard.  Meanwhile, `unsafeCoerce` may be
 needed.

 I am ''trying'' to go the `unsafeCoerce` route. But I have not succeeded
 to write it yet. I keep getting kind mismatch errors in line 27. So I
 replaced the call to `d` there with a hole `_`. Then I get this
 diagnostic:
 {{{
 9725.hs:27:30:
     Found hole  _  with type: Fac (ent k1) -> Fm (Fac (ent b0))
     Where:  ent  is a rigid type variable bound by
                  the type signature for
                    test :: (forall (i :: k). Kn (ent i) => Fm (Fac (ent
 i)))
                            -> Co Fm (O ent)
                  at
 /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:24:16
             k1  is a rigid type variable bound by
                 a pattern with constructor
                   Hi :: forall (k :: BOX) (ent :: k -> En) (k :: k).
                         Fac (ent k) -> O ent,
                 in an equation for  h
                 at
 /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:27:14
             b0  is an ambiguous type variable
     Relevant bindings include
       m :: Fac (ent k1)
         (bound at
 /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:27:17)
       h :: O ent -> Fm (O ent)
         (bound at
 /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:27:11)
       d :: forall (i :: k). Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i))
         (bound at
 /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:29:11)
       de :: forall (i :: k). Kn (ent i) => Fm (Fac (ent i))
         (bound at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:25:6)
       test :: (forall (i :: k). Kn (ent i) => Fm (Fac (ent i)))
               -> Co Fm (O ent)
         (bound at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:25:1)
     In the expression: _
     In the first argument of  HiF , namely  (_ m)
     In the expression: HiF (_ m)
 Failed, modules loaded: none.
 }}}
 Stangely the type reported for `m` is `Fac (ent k1)` (which comes from the
 context provided by `Hi` and not from the context provided by `Mo`, which
 would be `Fac (M b)`.
 This changes to the expected one with the "restricted" signature. I
 believe this is the place where the "badness" happens. Does this finding
 change something w.r.t. the analysis?

 >
 > Simon

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9725#comment:14>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler