Add valid refinement substitution suggestions for typed holes

This adds valid refinement substitution suggestions for typed holes and
documentation thereof.

Inspired by Agda's refinement facilities, this extends the typed holes
feature to be able to search for valid refinement substitutions, which
are substitutions that have one or more holes in them.

When the flag `-frefinement-level-substitutions=n` where `n > 0` is
passed, we also look for valid refinement substitutions, i.e.
substitutions that are valid, but adds more holes. Consider the
following:

  f :: [Integer] -> Integer
  f = _

Here the valid substitutions suggested will be (with the new
`-funclutter-valid-substitutions` flag for less verbosity set):

```
  Valid substitutions include
    f :: [Integer] -> Integer
    product :: forall (t :: * -> *).
              Foldable t => forall a. Num a => t a -> a
    sum :: forall (t :: * -> *).
          Foldable t => forall a. Num a => t a -> a
    maximum :: forall (t :: * -> *).
              Foldable t => forall a. Ord a => t a -> a
    minimum :: forall (t :: * -> *).
              Foldable t => forall a. Ord a => t a -> a
    head :: forall a. [a] -> a
    (Some substitutions suppressed; use -fmax-valid-substitutions=N or
-fno-max-valid-substitutions)
```

When the `-frefinement-level-substitutions=1` flag is given, we
additionally compute and report valid refinement substitutions:

```
  Valid refinement substitutions include
    foldl1 _ :: forall (t :: * -> *).
                Foldable t => forall a. (a -> a -> a) -> t a -> a
    foldr1 _ :: forall (t :: * -> *).
                Foldable t => forall a. (a -> a -> a) -> t a -> a
    head _ :: forall a. [a] -> a
    last _ :: forall a. [a] -> a
    error _ :: forall (a :: TYPE r).
                GHC.Stack.Types.HasCallStack => [Char] -> a
    errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
    (Some refinement substitutions suppressed; use
-fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
```

Which are substitutions with holes in them. This allows e.g. beginners
to discover the fold functions and similar.

We find these refinement suggestions by considering substitutions that
don't fit the type of the hole, but ones that would fit if given an
additional argument. We do this by creating a new type variable with
newOpenFlexiTyVarTy (e.g. `t_a1/m[tau:1]`), and then considering
substitutions of the type `t_a1/m[tau:1] -> v` where `v` is the type of
the hole. Since the simplifier is free to unify this new type variable
with any type (and it is cloned before each check to avoid
side-effects), we can now discover any identifiers that would fit if
given another identifier of a suitable type. This is then generalized
so that we can consider any number of additional arguments by setting
the `-frefinement-level-substitutions` flag to any number, and then
considering substitutions like e.g. `foldl _ _` with two additional
arguments.

This can e.g. help beginners discover the `fold` functions.
This could also help more advanced users figure out which morphisms
they can use when arrow chasing.
Then you could write `m = _ . m2 . m3` where `m2` and `m3` are some
morphisms, and not only get exact fits, but also help in finding
morphisms that might get you a little bit closer to where you want to
go in the diagram.

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

Differential Revision: https://phabricator.haskell.org/D4357

1 files changed, 114 insertions, 2 deletions

diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index d213a5cdba..439f4d2555 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -11051,6 +11051,12 @@ for typed holes:
                 (imported from ‘Prelude’ at show_constraints.hs:1:8-11
                 (and originally defined in ‘GHC.Err’))
 
+.. _typed-hole-valid-substitutions:
+
+Valid Substitutions
+-------------------
+GHC sometimes suggests valid substitutions for typed holes, which is
+configurable by a few flags.
 
 .. ghc-flag:: -fno-show-valid-substitutions
     :shortdesc: Disables showing a list of valid substitutions for typed holes
@@ -11146,9 +11152,115 @@ for typed holes:
 
     The list of valid substitutions is limited by displaying up to 6
     substitutions per hole. The number of substitutions shown can be set by this
-    flag. Turning the limit off with ``-fno-max-valid-substitutions`` displays
-    all the found substitutions. 
+    flag. Turning the limit off with :ghc-flag:`-fno-max-valid-substitutions`
+    displays all found substitutions.
+
+.. ghc-flag:: -funclutter-valid-substitutions
+    :shortdesc: Unclutter the list of valid substitutions by not showing
+        provenance of suggestion.
+    :type: dynamic
+    :category: verbosity
+
+    :default: off
+
+    This flag can be toggled to decrease the verbosity of the valid
+    substitution suggestions by not showing the provenance the suggestions.
+
+.. _typed-holes-refinement-substitutions:
+
+Refinement Substitutions
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+When the flag :ghc-flag:`-frefinement-level-substitutions=⟨n⟩` is set to an
+``n`` larger than ``0``, GHC will offer up a list of valid refinement
+substitutions, which are valid substitutions that need up to ``n`` levels of
+additional refinement to be complete, where each level represents an additional
+hole in the substitution that requires filling in.  As an example, consider the
+hole in ::
+
+  f :: [Integer] -> Integer
+  f = _
+
+When the refinement level is not set, it will only offer valid substitutions
+suggestions: ::
+
+  Valid substitutions include
+    f :: [Integer] -> Integer
+    product :: forall (t :: * -> *).
+              Foldable t => forall a. Num a => t a -> a
+    sum :: forall (t :: * -> *).
+          Foldable t => forall a. Num a => t a -> a
+    maximum :: forall (t :: * -> *).
+              Foldable t => forall a. Ord a => t a -> a
+    minimum :: forall (t :: * -> *).
+              Foldable t => forall a. Ord a => t a -> a
+    head :: forall a. [a] -> a
+    (Some substitutions suppressed; use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
+
+However, with :ghc-flag:`-frefinement-level-substitutions=⟨n⟩` set to e.g. `1`,
+it will additionally offer up a list of refinement substitutions, in this case: ::
+
+  Valid refinement substitutions include
+    foldl1 _ :: forall (t :: * -> *).
+                Foldable t => forall a. (a -> a -> a) -> t a -> a
+    foldr1 _ :: forall (t :: * -> *).
+                Foldable t => forall a. (a -> a -> a) -> t a -> a
+    head _ :: forall a. [a] -> a
+    last _ :: forall a. [a] -> a
+    error _ :: forall (a :: TYPE r).
+                GHC.Stack.Types.HasCallStack => [Char] -> a
+    errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
+    (Some refinement substitutions suppressed;
+      use -fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
+
+Which shows that the hole could be replaced with e.g. ``foldl1 _``. While not
+fixing the hole, this can help users understand what options they have.
+ 
+.. ghc-flag:: -frefinement-level-substitutions=⟨n⟩
+    :shortdesc: *default: off.* Sets the level of refinement of the
+         refinement substitutions, where level ``n`` means that substitutions
+         of up to ``n`` holes will be considered.
+    :type: dynamic
+    :reverse: -fno-refinement-level-substitutions
+    :category: verbosity
 
+    :default: off
+
+    The list of valid refinement substitutions is generated by considering
+    substitutions with a varying amount of additional holes. The amount of
+    holes in a refinement can be set by this flag. If the flag is set to 0
+    or not set at all, no valid refinement substitutions will be suggested.
+
+.. ghc-flag:: -fabstract-refinement-substitutions
+    :shortdesc: *default: off.* Toggles whether refinements where one or more
+         or more of the holes are abstract are reported.
+    :type: dynamic
+    :reverse: -fno-abstract-refinement-substitutions
+    :category: verbosity
+
+    :default: off
+
+    Valid list of valid refinement substitutions can often grow large when
+    the refinement level is ``>= 2``, with holes like ``head _ _`` or
+    ``fst _ _``, which are valid refinements, but which are unlikely to be
+    relevant since one or more of the holes are still completely open, in that
+    neither the type nor kind of those holes are constrained by the proposed
+    identifier at all. By default, such holes are not reported. By turning this
+    flag on, such holes are included in the list of valid refinement substitutions.
+
+.. ghc-flag:: -fmax-refinement-substitutions=⟨n⟩
+    :shortdesc: *default: 6.* Set the maximum number of refinement substitutions
+         for typed holes to display in type error messages.
+    :type: dynamic
+    :reverse: -fno-max-refinement-substitutions
+    :category: verbosity
+
+    :default: 6
+
+    The list of valid refinement substitutions is limited by displaying up to 6
+    substitutions per hole. The number of substitutions shown can be set by this
+    flag. Turning the limit off with :ghc-flag:`-fno-max-refinement-substitutions`
+    displays all found substitutions.
 
 .. _partial-type-signatures: