search

yav / type-nat-solver

A plugin for solving numeric constraints in GHC's type-checker
Other
50 stars 5 forks source link

`mkNewFact` is not compatible with GHC HEAD #4

Closed plaidfinch closed 8 years ago

plaidfinch commented 8 years ago

In attempting to compile the plugin for GHC HEAD, I get only one compile error, for the function mkNewFact:

mkNewFact :: CtLoc -> Bool -> (Type,Type) -> CtEvidence
mkNewFact newLoc withEv (t1,t2)
  | withEv = CtGiven { ctev_pred = newPred
                     , ctev_evtm = evBy (t1,t2)
                     , ctev_loc  = newLoc
                     }
  | otherwise = CtDerived { ctev_pred = newPred
                          , ctev_loc  = newLoc
                          }
  where
  newPred = mkEqPred t1 t2

The problem is that the ctev_evtm field of the CtGiven constructor on the CtEvidence type has changed; it is now ctev_evar, of type EvVar, while it used to be of type EvTerm. I believe this is due to changes in the constraint solver architecture for GHC 8.0—@goldfirere would know more about this, I'm pretty sure.

In any case, we need to find a way to shoe-horn the manufactured evidence into an EvVar now. I'm not sure which bits of the EvVar infrastructure should be used to replicate the previous behavior; any ideas?

adamgundry commented 8 years ago

The TcPluginM module of the GHC API now exports newWanted/newGiven/newDerived functions that should help here. You might also be interested in ghc-tcplugins-extra, which is intended to contain common functionality for plugins and to paper over the differences between different versions of the GHC API.

plaidfinch commented 8 years ago

Works perfectly; thanks @adamgundry. I just submitted a pull request with this patch.