Commit 1c92f193 authored by Matthías Páll Gissurarson's avatar Matthías Páll Gissurarson Committed by Ben Gamari

Add built-in syntax suggestions, and refactor to allow library use

Summary:
This change to the valid hole fits adds built-in syntax candidates (like (:) and []),
so that they are checked in addition to what is in scope.

The rest is merely a refactor and export of the functions used to find the valid
hole fits, since there was interest at ICFP to use the valid hole fit machinery for
additional uses. By exporting the `tcFilterHoleFits` function, this can now be done
without having to rely on parsing the actual error message.

Test Plan: Test for built-in syntax included

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: RyanGlScott, rwbarton, carter

Differential Revision: https://phabricator.haskell.org/D5227
parent 695f1f2f
This diff is collapsed.
......@@ -41,15 +41,16 @@ T14273.hs:7:32: warning: [-Wtyped-holes (in -Wdefault)]
True :: Bool
(imported from ‘Prelude’ at T14273.hs:1:8-40
(and originally defined in ‘GHC.Types’))
EQ :: Ordering
LT :: Ordering
(imported from ‘Prelude’ at T14273.hs:1:8-40
(and originally defined in ‘GHC.Types’))
LT :: Ordering
EQ :: Ordering
(imported from ‘Prelude’ at T14273.hs:1:8-40
(and originally defined in ‘GHC.Types’))
GT :: Ordering
(imported from ‘Prelude’ at T14273.hs:1:8-40
(and originally defined in ‘GHC.Types’))
() :: () (bound at <wired into compiler>)
pi :: forall a. Floating a => a
with pi @Double
(imported from ‘Prelude’ at T14273.hs:1:8-40
......
......@@ -36,7 +36,7 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
where const :: forall a b. a -> b -> a
($) (_ :: [Integer] -> Integer)
where ($) :: forall a b. (a -> b) -> a -> b
fail (_ :: String)
fail (_ :: [Char])
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
return (_ :: Integer)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
......@@ -86,15 +86,15 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
where (<$) :: forall (f :: * -> *) a b.
Functor f =>
a -> f b -> f a
id (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
id (_ :: t1 -> [Integer] -> Integer) (_ :: t1)
where id :: forall a. a -> a
head (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
head (_ :: [t1 -> [Integer] -> Integer]) (_ :: t1)
where head :: forall a. [a] -> a
last (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
last (_ :: [t1 -> [Integer] -> Integer]) (_ :: t1)
where last :: forall a. [a] -> a
fst (_ :: (t0 -> [Integer] -> Integer, b2)) (_ :: t0)
fst (_ :: (t1 -> [Integer] -> Integer, b2)) (_ :: t1)
where fst :: forall a b. (a, b) -> a
snd (_ :: (a3, t0 -> [Integer] -> Integer)) (_ :: t0)
snd (_ :: (a3, t1 -> [Integer] -> Integer)) (_ :: t1)
where snd :: forall a b. (a, b) -> b
id (_ :: [Integer] -> Integer)
where id :: forall a. a -> a
......@@ -116,11 +116,11 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
where const :: forall a b. a -> b -> a
($) (_ :: a5 -> [Integer] -> Integer) (_ :: a5)
where ($) :: forall a b. (a -> b) -> a -> b
fail (_ :: String) (_ :: t0)
fail (_ :: [Char]) (_ :: t1)
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
return (_ :: [Integer] -> Integer) (_ :: t0)
return (_ :: [Integer] -> Integer) (_ :: t1)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
pure (_ :: [Integer] -> Integer) (_ :: t0)
pure (_ :: [Integer] -> Integer) (_ :: t1)
where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
uncurry (_ :: a4 -> b3 -> [Integer] -> Integer) (_ :: (a4, b3))
where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
......@@ -156,7 +156,7 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
where const :: forall a b. a -> b -> a
($) (_ :: Integer -> [Integer] -> Integer)
where ($) :: forall a b. (a -> b) -> a -> b
fail (_ :: String)
fail (_ :: [Char])
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
return (_ :: [Integer] -> Integer)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
......@@ -209,15 +209,15 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
where (<$) :: forall (f :: * -> *) a b.
Functor f =>
a -> f b -> f a
id (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
id (_ :: t1 -> Integer -> [Integer] -> Integer) (_ :: t1)
where id :: forall a. a -> a
head (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
head (_ :: [t1 -> Integer -> [Integer] -> Integer]) (_ :: t1)
where head :: forall a. [a] -> a
last (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
last (_ :: [t1 -> Integer -> [Integer] -> Integer]) (_ :: t1)
where last :: forall a. [a] -> a
fst (_ :: (t0 -> Integer -> [Integer] -> Integer, b2)) (_ :: t0)
fst (_ :: (t1 -> Integer -> [Integer] -> Integer, b2)) (_ :: t1)
where fst :: forall a b. (a, b) -> a
snd (_ :: (a3, t0 -> Integer -> [Integer] -> Integer)) (_ :: t0)
snd (_ :: (a3, t1 -> Integer -> [Integer] -> Integer)) (_ :: t1)
where snd :: forall a b. (a, b) -> b
id (_ :: Integer -> [Integer] -> Integer)
where id :: forall a. a -> a
......@@ -240,11 +240,11 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
where const :: forall a b. a -> b -> a
($) (_ :: a5 -> Integer -> [Integer] -> Integer) (_ :: a5)
where ($) :: forall a b. (a -> b) -> a -> b
fail (_ :: String) (_ :: t0)
fail (_ :: [Char]) (_ :: t1)
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
return (_ :: Integer -> [Integer] -> Integer) (_ :: t1)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
pure (_ :: Integer -> [Integer] -> Integer) (_ :: t1)
where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
uncurry (_ :: a4 -> b3 -> Integer -> [Integer] -> Integer)
(_ :: (a4, b3))
......
......@@ -37,7 +37,7 @@ constraint_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
where const :: forall a b. a -> b -> a
($) (_ :: [a] -> a)
where ($) :: forall a b. (a -> b) -> a -> b
fail (_ :: String)
fail (_ :: [Char])
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
return (_ :: a)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
......
......@@ -43,6 +43,7 @@ hole_constraints.hs:16:35: warning: [-Wtyped-holes (in -Wdefault)]
Valid hole fits include
f3 :: [a]
f1 :: forall a. Eq a => a
[] :: forall a. [a]
mempty :: forall a. Monoid a => a
hole_constraints.hs:20:19: warning: [-Wtyped-holes (in -Wdefault)]
......@@ -73,4 +74,5 @@ hole_constraints.hs:27:32: warning: [-Wtyped-holes (in -Wdefault)]
f3 :: forall a. C a => a
f1 :: forall a. Eq a => a
f2 :: forall a. (Show a, Eq a) => a
[] :: forall a. [a]
mempty :: forall a. Monoid a => a
......@@ -30,6 +30,7 @@ holes.hs:8:5: warning: [-Wtyped-holes (in -Wdefault)]
Valid hole fits include
h :: [Char]
f :: forall t. t
[] :: forall a. [a]
mempty :: forall a. Monoid a => a
holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
......@@ -50,6 +51,10 @@ holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
otherwise :: Bool
False :: Bool
True :: Bool
LT :: Ordering
EQ :: Ordering
GT :: Ordering
() :: ()
lines :: String -> [String]
unlines :: [String] -> String
unwords :: [String] -> String
......@@ -72,9 +77,6 @@ holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
(&&) :: Bool -> Bool -> Bool
not :: Bool -> Bool
(||) :: Bool -> Bool -> Bool
EQ :: Ordering
LT :: Ordering
GT :: Ordering
(++) :: forall a. [a] -> [a] -> [a]
filter :: forall a. (a -> Bool) -> [a] -> [a]
fromInteger :: forall a. Num a => Integer -> a
......@@ -84,8 +86,10 @@ holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
fromIntegral :: forall a b. (Integral a, Num b) => a -> b
toInteger :: forall a. Integral a => a -> Integer
toRational :: forall a. Real a => a -> Rational
(:) :: forall a. a -> [a] -> [a]
Nothing :: forall a. Maybe a
Just :: forall a. a -> Maybe a
[] :: forall a. [a]
asTypeOf :: forall a. a -> a -> a
id :: forall a. a -> a
until :: forall a. (a -> Bool) -> (a -> a) -> a -> a
......@@ -166,6 +170,8 @@ holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
snd :: forall a b. (a, b) -> b
map :: forall a b. (a -> b) -> [a] -> [b]
realToFrac :: forall a b. (Real a, Fractional b) => a -> b
Left :: forall a b. a -> Either a b
Right :: forall a b. b -> Either a b
maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
const :: forall a b. a -> b -> a
scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
......@@ -179,8 +185,6 @@ holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
a -> (b, a)
round :: forall a b. (RealFrac a, Integral b) => a -> b
truncate :: forall a b. (RealFrac a, Integral b) => a -> b
Right :: forall a b. b -> Either a b
Left :: forall a b. a -> Either a b
($) :: forall a b. (a -> b) -> a -> b
either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
......
......@@ -26,7 +26,8 @@ holes2.hs:3:10: warning: [-Wtyped-holes (in -Wdefault)]
otherwise :: Bool
False :: Bool
True :: Bool
EQ :: Ordering
LT :: Ordering
EQ :: Ordering
GT :: Ordering
() :: ()
pi :: forall a. Floating a => a
......@@ -32,6 +32,7 @@ holes3.hs:8:5: error:
Valid hole fits include
h :: [Char]
f :: forall t. t
[] :: forall a. [a]
mempty :: forall a. Monoid a => a
holes3.hs:11:15: error:
......@@ -53,6 +54,10 @@ holes3.hs:11:15: error:
otherwise :: Bool
False :: Bool
True :: Bool
LT :: Ordering
EQ :: Ordering
GT :: Ordering
() :: ()
lines :: String -> [String]
unlines :: [String] -> String
unwords :: [String] -> String
......@@ -75,9 +80,6 @@ holes3.hs:11:15: error:
(&&) :: Bool -> Bool -> Bool
not :: Bool -> Bool
(||) :: Bool -> Bool -> Bool
EQ :: Ordering
LT :: Ordering
GT :: Ordering
(++) :: forall a. [a] -> [a] -> [a]
filter :: forall a. (a -> Bool) -> [a] -> [a]
fromInteger :: forall a. Num a => Integer -> a
......@@ -87,8 +89,10 @@ holes3.hs:11:15: error:
fromIntegral :: forall a b. (Integral a, Num b) => a -> b
toInteger :: forall a. Integral a => a -> Integer
toRational :: forall a. Real a => a -> Rational
(:) :: forall a. a -> [a] -> [a]
Nothing :: forall a. Maybe a
Just :: forall a. a -> Maybe a
[] :: forall a. [a]
asTypeOf :: forall a. a -> a -> a
id :: forall a. a -> a
until :: forall a. (a -> Bool) -> (a -> a) -> a -> a
......@@ -169,6 +173,8 @@ holes3.hs:11:15: error:
snd :: forall a b. (a, b) -> b
map :: forall a b. (a -> b) -> [a] -> [b]
realToFrac :: forall a b. (Real a, Fractional b) => a -> b
Left :: forall a b. a -> Either a b
Right :: forall a b. b -> Either a b
maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
const :: forall a b. a -> b -> a
scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
......@@ -182,8 +188,6 @@ holes3.hs:11:15: error:
a -> (b, a)
round :: forall a b. (RealFrac a, Integral b) => a -> b
truncate :: forall a b. (RealFrac a, Integral b) => a -> b
Right :: forall a b. b -> Either a b
Left :: forall a b. a -> Either a b
($) :: forall a b. (a -> b) -> a -> b
either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
......
......@@ -71,7 +71,7 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
(and originally defined in ‘GHC.Base’))
fail (_ :: String)
fail (_ :: [Char])
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
with fail @((->) [Integer]) @Integer
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
......@@ -172,7 +172,7 @@ refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
with ($) @'GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
(and originally defined in ‘GHC.Base’))
fail (_ :: String)
fail (_ :: [Char])
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
with fail @((->) Integer) @([Integer] -> Integer)
(imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
......
......@@ -10,20 +10,23 @@ type_in_type_hole_fits.hs:79:11: warning: [-Wtyped-holes (in -Wdefault)]
mySortA :: Sorted (O (N ^. 2)) (O N) 'True Integer
(bound at type_in_type_hole_fits.hs:79:1)
Valid hole fits include
mergeSort :: forall a (n :: AsympPoly) (m :: AsympPoly) (s :: Bool).
Sorted :: forall (cpu :: AsympPoly) (mem :: AsympPoly)
(stable :: Bool) a.
[a] -> Sorted cpu mem stable a
with Sorted @(O ('NLogN 2 0)) @(O N) @'True @Integer
(defined at type_in_type_hole_fits.hs:54:18)
mergeSort :: forall a (n :: AsympPoly) (m :: AsympPoly)
(s :: Bool).
(Ord a, n >=. O (N *. LogN), m >=. O N, IsStable s) =>
[a] -> Sorted n m s a
with mergeSort @Integer @(O ('NLogN 2 0)) @(O N) @'True
(defined at type_in_type_hole_fits.hs:61:1)
insertionSort :: forall a (n :: AsympPoly) (m :: AsympPoly) (s :: Bool).
insertionSort :: forall a (n :: AsympPoly) (m :: AsympPoly)
(s :: Bool).
(Ord a, n >=. O (N ^. 2), m >=. O One, IsStable s) =>
[a] -> Sorted n m s a
with insertionSort @Integer @(O ('NLogN 2 0)) @(O N) @'True
(defined at type_in_type_hole_fits.hs:65:1)
Sorted :: forall (cpu :: AsympPoly) (mem :: AsympPoly) (stable :: Bool) a.
[a] -> Sorted cpu mem stable a
with Sorted @(O ('NLogN 2 0)) @(O N) @'True @Integer
(defined at type_in_type_hole_fits.hs:54:18)
type_in_type_hole_fits.hs:82:11: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole:
......@@ -46,15 +49,17 @@ type_in_type_hole_fits.hs:82:11: warning: [-Wtyped-holes (in -Wdefault)]
[a] -> Sorted n m 'False a
with heapSort @Integer @(O ('NLogN 1 1)) @(O N)
(defined at type_in_type_hole_fits.hs:74:1)
mergeSort :: forall a (n :: AsympPoly) (m :: AsympPoly) (s :: Bool).
Sorted :: forall (cpu :: AsympPoly) (mem :: AsympPoly)
(stable :: Bool) a.
[a] -> Sorted cpu mem stable a
with Sorted @(O ('NLogN 1 1)) @(O N) @'False @Integer
(defined at type_in_type_hole_fits.hs:54:18)
mergeSort :: forall a (n :: AsympPoly) (m :: AsympPoly)
(s :: Bool).
(Ord a, n >=. O (N *. LogN), m >=. O N, IsStable s) =>
[a] -> Sorted n m s a
with mergeSort @Integer @(O ('NLogN 1 1)) @(O N) @'False
(defined at type_in_type_hole_fits.hs:61:1)
Sorted :: forall (cpu :: AsympPoly) (mem :: AsympPoly) (stable :: Bool) a.
[a] -> Sorted cpu mem stable a
with Sorted @(O ('NLogN 1 1)) @(O N) @'False @Integer
(defined at type_in_type_hole_fits.hs:54:18)
type_in_type_hole_fits.hs:85:11: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole:
......@@ -72,7 +77,8 @@ type_in_type_hole_fits.hs:85:11: warning: [-Wtyped-holes (in -Wdefault)]
[a] -> Sorted n m 'False a
with heapSort @Integer @(O ('NLogN 1 1)) @(O One)
(defined at type_in_type_hole_fits.hs:74:1)
Sorted :: forall (cpu :: AsympPoly) (mem :: AsympPoly) (stable :: Bool) a.
Sorted :: forall (cpu :: AsympPoly) (mem :: AsympPoly)
(stable :: Bool) a.
[a] -> Sorted cpu mem stable a
with Sorted @(O ('NLogN 1 1)) @(O One) @'False @Integer
(defined at type_in_type_hole_fits.hs:54:18)
......@@ -33,5 +33,9 @@ f = show _
h :: String
h = show (_ (_ :: Bool))
-- Built-in Syntax
myCons :: a -> [a] -> [a]
myCons = _
main :: IO ()
main = _ "hello, world"
......@@ -109,15 +109,16 @@ valid_hole_fits.hs:30:10: warning: [-Wtyped-holes (in -Wdefault)]
True :: Bool
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Types’))
EQ :: Ordering
LT :: Ordering
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Types’))
LT :: Ordering
EQ :: Ordering
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Types’))
GT :: Ordering
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Types’))
() :: () (bound at <wired into compiler>)
pi :: forall a. Floating a => a
with pi @Double
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
......@@ -194,13 +195,41 @@ valid_hole_fits.hs:34:14: warning: [-Wtyped-holes (in -Wdefault)]
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Enum’))
valid_hole_fits.hs:37:8: warning: [-Wtyped-holes (in -Wdefault)]
valid_hole_fits.hs:38:10: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: a -> [a] -> [a]
Where: ‘a’ is a rigid type variable bound by
the type signature for:
myCons :: forall a. a -> [a] -> [a]
at valid_hole_fits.hs:37:1-25
• In the expression: _
In an equation for ‘myCons’: myCons = _
• Relevant bindings include
myCons :: a -> [a] -> [a] (bound at valid_hole_fits.hs:38:1)
Valid hole fits include
myCons :: a -> [a] -> [a] (bound at valid_hole_fits.hs:38:1)
(:) :: forall a. a -> [a] -> [a]
with (:) @a
(bound at <wired into compiler>)
(<$) :: forall (f :: * -> *) a b. Functor f => a -> f b -> f a
with (<$) @[] @a @a
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Base’))
seq :: forall a b. a -> b -> b
with seq @a @[a]
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Prim’))
mempty :: forall a. Monoid a => a
with mempty @(a -> [a] -> [a])
(imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
(and originally defined in ‘GHC.Base’))
valid_hole_fits.hs:41:8: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: [Char] -> IO ()
• In the expression: _
In the expression: _ "hello, world"
In an equation for ‘main’: main = _ "hello, world"
• Relevant bindings include
main :: IO () (bound at valid_hole_fits.hs:37:1)
main :: IO () (bound at valid_hole_fits.hs:41:1)
Valid hole fits include
ps :: String -> IO () (defined at valid_hole_fits.hs:9:1)
System.IO.putStr :: String -> IO ()
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment