• Matthías Páll Gissurarson's avatar
    Add valid refinement substitution suggestions for typed holes · 918c0b39
    Matthías Páll Gissurarson authored
    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
    918c0b39
TcErrors.hs 141 KB