[commit: ghc] master: Add valid refinement substitution suggestions for typed holes (918c0b3)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/918c0b393663e88f89becdb8520de477ce6a5463/ghc

>---------------------------------------------------------------

commit 918c0b393663e88f89becdb8520de477ce6a5463
Author: Matthías Páll Gissurarson <mpg at mpg.is>
Date:   Sun Feb 18 11:01:06 2018 -0500

    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


>---------------------------------------------------------------

918c0b393663e88f89becdb8520de477ce6a5463
 compiler/main/DynFlags.hs                          |  20 ++
 compiler/typecheck/TcErrors.hs                     | 290 ++++++++++++++++-----
 compiler/typecheck/TcRnTypes.hs                    |  16 +-
 docs/users_guide/glasgow_exts.rst                  | 116 ++++++++-
 .../abstract_refinement_substitutions.hs           |   7 +
 .../abstract_refinement_substitutions.stderr       | 290 +++++++++++++++++++++
 testsuite/tests/typecheck/should_compile/all.T     |   2 +
 .../should_compile/refinement_substitutions.hs     |   7 +
 .../should_compile/refinement_substitutions.stderr | 188 +++++++++++++
 9 files changed, 857 insertions(+), 79 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc 918c0b393663e88f89becdb8520de477ce6a5463