[GHC] #5910: Holes with other constraints

[GHC]

#5910: Holes with other constraints
----------------------------------------+-----------------------------------
    Reporter:  xnyhps                   |       Owner:                  
        Type:  feature request          |      Status:  new             
    Priority:  normal                   |   Milestone:                  
   Component:  Compiler (Type checker)  |     Version:  7.5             
    Keywords:  holes                    |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple         |     Failure:  Other           
  Difficulty:  Unknown                  |    Testcase:                  
   Blockedby:                           |    Blocking:                  
     Related:                           |  
----------------------------------------+-----------------------------------

Comment(by simonpj):

 Replying to [comment:14 xnyhps]:

 >  * I've thought about this a lot, and went through the code, but I'm
 still not sure about your advice about `HolePred` and `HoleTyCon`. Right
 now, `tcExpr` emits a constraint (which is just a `Type`) when
 encountering a hole. Without `HoleTyCon`, I'm not sure how to find out a
 constraint was a hole-constraint, which is needed for it to turn into an
 `CHoleCan`. `classifyPredType` will reduce anything it doesn't recognize
 to a `IrredPred`, in which case it never solves anything. `canEvVar` (with
 `canHole`) needs to see a `HolePred` to make it an `CHoleCan`.

 No, I mean something very simple, roughly like this:
 {{{
 tcExpr (HoleExpr hole_name _) res_ty
  = do { loc <- getCtLoc (HoleOrigin hole_name)
       ; emitFlat (CHoleCan res_ty loc)
       ; return (HoleExpr hole_name res_ty) }
 }}}
 What is happening here is this:
  * We are type-checking a hole, expecting it to have type `res_ty`
  * Fine!  We assume it does have that type (that is, no unification or
 whatnot)
  * But we emit a `CHoleCan` constraint which will later (in `TcErrors`)
 report that the hole `_?x` should have type `res_ty`.

 And that's about all really.  No messing with `TyCons`, no special
 predicates, nothing.

 Now it is true that these hole constraints are a bit unusual in that they
 don't have evidence, and there isn't a `PredType`.  But I don't think that
 will be hard: in the solver you just want to put them in the "frozen
 errors" set; indeed you can put them there right away.  Currently we have
 `emitFlat` and `emitImplication`; just add `emitInsoluble` which adds to
 the `wc_insol` field of the `WantedConstraints`.

 I think it's all delightfully simple.  But of course I coudld be wrong.

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