This hole plugin shows how djinn can be invoked by a hole fit plugin to synthesize simple programs.
DjinnBridge is based on the djinn-ghc package by Alejandro Serrano but modified to use TcM directly.
Note! Needs GHC 8.10
Using this plugin, you can compile the following:
{-# OPTIONS -fplugin=DjinnPlugin -funclutter-valid-hole-fits #-}
module Main where
f :: a -> a
f = _
g :: a -> b -> b
g = _
i :: (a,b) -> a
i = _
j :: a -> a -> a
j = _
main :: IO ()
main = return ()And get the following output:
Main.hs:5:5: error:
• Found hole: _ :: a -> a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a. a -> a
at Main.hs:4:1-12
• In the expression: _
In an equation for ‘f’: f = _
• Relevant bindings include f :: a -> a (bound at Main.hs:5:1)
Valid hole fits include
(\ a -> a)
(\ _ -> head (cycle (([]) ++ ([]))))
(\ _ -> id (head (cycle (([]) ++ ([])))))
f :: a -> a
id :: forall a. a -> a
|
5 | f = _
| ^
Main.hs:8:5: error:
• Found hole: _ :: a -> b -> b
Where: ‘a’, ‘b’ are rigid type variables bound by
the type signature for:
g :: forall a b. a -> b -> b
at Main.hs:7:1-16
• In the expression: _
In an equation for ‘g’: g = _
• Relevant bindings include g :: a -> b -> b (bound at Main.hs:8:1)
Valid hole fits include
(\ _ a -> a)
(\ _ a -> seq (head (cycle (([]) ++ ([])))) a)
(\ _ a -> snd (head (cycle (([]) ++ ([]))), a))
g :: a -> b -> b
seq :: forall a b. a -> b -> b
|
8 | g = _
| ^
Main.hs:11:5: error:
• Found hole: _ :: (a, b) -> a
Where: ‘b’, ‘a’ are rigid type variables bound by
the type signature for:
i :: forall a b. (a, b) -> a
at Main.hs:10:1-15
• In the expression: _
In an equation for ‘i’: i = _
• Relevant bindings include
i :: (a, b) -> a (bound at Main.hs:11:1)
Valid hole fits include
(\ (a, _) -> a)
(\ _ -> head (cycle (([]) ++ ([]))))
(\ _ -> f (head (cycle (([]) ++ ([])))))
i :: (a, b) -> a
fst :: forall a b. (a, b) -> a
|
11 | i = _
| ^
Main.hs:14:5: error:
• Found hole: _ :: a -> a -> a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
j :: forall a. a -> a -> a
at Main.hs:13:1-16
• In the expression: _
In an equation for ‘j’: j = _
• Relevant bindings include
j :: a -> a -> a (bound at Main.hs:14:1)
Valid hole fits include
(\ _ a -> a)
(\ a _ -> a)
(\ _ _ -> head (cycle (([]) ++ ([]))))
j :: a -> a -> a
g :: forall a b. a -> b -> b
seq :: forall a b. a -> b -> b
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
|
14 | j = _
| ^