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, 8 insertions, 8 deletions

diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index d2c8dd8a43..4b11fa6114 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -2592,17 +2592,17 @@ pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
 
 -- | Wraps the given type with the constraints (via ic_given) in the given
 -- implication, according to the variables mentioned (via ic_skols)
--- in the implication.
+-- in the implication, but taking care to only wrap those variables
+-- that are mentioned in the type or the implication.
 wrapTypeWithImplication :: Type -> Implication -> Type
-wrapTypeWithImplication ty impl =
-  wrapType ty (ic_skols impl) (map idType $ ic_given impl)
+wrapTypeWithImplication ty impl = wrapType ty mentioned_skols givens
+    where givens = map idType $ ic_given impl
+          skols = ic_skols impl
+          freeVars = fvVarSet $ tyCoFVsOfTypes (ty:givens)
+          mentioned_skols = filter (`elemVarSet` freeVars) skols
 
 wrapType :: Type -> [TyVar] -> [PredType] -> Type
-wrapType ty skols givens =
-    wrapWithAllSkols $ mkFunTys givens ty
-    where forAllTy :: Type -> TyVar -> Type
-          forAllTy ty tv = mkForAllTy tv Specified ty
-          wrapWithAllSkols ty = foldl forAllTy ty skols
+wrapType ty skols givens = mkSpecForAllTys skols $ mkFunTys givens ty
 
 
 {-