Nested Implications

Simon Peyton Jones simonpj at microsoft.com
Mon Apr 16 12:51:59 UTC 2018


Mathias

I suspect substImplication was removed simply because it was never called, but I’m not certain.

The entire cloning and substitution business is very heavyweight.  Here’s an alternative idea:


  *   Gather ‘fuvs’, the set of all free unification variables of the constraint you are about to solve.
  *   Solve the constraint
  *   For each variable in ‘fuvs’, set its IORef to Flexi; that is, simply undo any unification that has taken place.

That seems simple, very non-invasive, and robust.

Simon

From: Matthías Páll Gissurarson <pallm at student.chalmers.se>
Sent: 10 April 2018 00:57
To: Simon Peyton Jones <simonpj at microsoft.com>
Subject: Nested Implications

Greetings Simon,

I've been working on implementing the valid substitutions for typed holes in terms of nested implications, and I think I've worked out how to do it. But one thing bothers me. To use the implications that are passed along with the ReportErrCtxt, I have to clone the type variables within, to avoid having side-effects that could impact later searches. I clone the type variables and create a substitution from the old variables to the new, which I'd like to apply to the implication. When I was looking around for how to do that, I came across this code in GHC 7.6.3

https://downloads.haskell.org/~ghc/7.6-latest/docs/html/libraries/ghc-7.6.3/src/Inst.html<https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2F7.6-latest%2Fdocs%2Fhtml%2Flibraries%2Fghc-7.6.3%2Fsrc%2FInst.html&data=02%7C01%7Csimonpj%40microsoft.com%7Cebcb3f452d22449ccd4d08d59e75a6d7%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636589150506893746&sdata=y188p6jNMD4%2Bd1eHVhxBhIdSq2RDgrytpfNmkGG8WUk%3D&reserved=0>

The `substImplication` function does precisely what I want, i.e. applies a substitution to an implication. However, that code is no longer present in GHC 8.5! The git history doesn't go far enough back for me to find an explanation, so I wanted to ask: why was this function removed? Is there something I should be wary of if I re-implement it?

Please correct me if my approach is all wrong, I'd like to hear what you had in mind.
--
-

Matthías Páll Gissurarson
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180416/4370a015/attachment.html>


More information about the ghc-devs mailing list