[GHC] #15613: GHCi command, tracing steps of instance resolution for Constraint or expression

[GHC]

#15613: GHCi command, tracing steps of instance resolution for Constraint or
expression
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  lowest            |            Milestone:
       Component:  GHCi              |              Version:
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15610            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

Old description:

> Another GHCi command (#15610), `:elab <constraint>` traces instance
> resolution for `<constraint>`. This is already something people do by
> hand (ticket:10318#comment:6) and would be a great tool for explorers of
> Haskell
>
> {{{
> >> :elab Monoid (a -> b -> ([c], Sum Int))
> Monoid (a -> b -> ([c], Sum Int))
> ==> Monoid (b -> ([c], Sum Int))
>   ==> Monoid ([c], Sum Int)
>     ==> Monoid [c]
>     ==> Monoid (Sum Int)
>       ==> Num Int
> }}}
>
> If resolving the type class fails, it can pinpoint what caused it to fail
>
> {{{
> >> data A
> >> :elab Show (A, Int -> Int)
> Show (A, Int -> Int)
> <~bRZsz NO instance~>
>
> ==> Show A
>   <NO instance>
> ==> Show (Int -> Int)
>   <NO instance>
> }}}
>
> A verbose version can explain each step
>
> {{{
> >> :elab +v Monoid (a -> b -> ([c], Sum Int)
> Monoid (a -> b -> ([c], Sum Int)) -- Monoid b => Monoid (a -> b)
> (‘GHC.Base’)
> ==> Monoid (b -> ([c], Sum Int))  -- Monoid b => Monoid (a -> b)
> (‘GHC.Base’)
>   ==> Monoid ([c], Sum Int)       -- Monoid b => Monoid (a -> b)
> (‘GHC.Base’)
>     ==> Monoid [c]                --             Monoid [a]
> (‘GHC.Base’)
>     ==> Monoid (Sum Int)          -- Num    a => Monoid (Sum a)
> (‘Data.Monoid’)
>       ==> Num Int                 --             Num Int
> (‘GHC.Num’)
> }}}
>
> {{{
> >> :elab +v Num (Int, Float, Rational)
> Num (Int, Float, Rational) --  (Num a, Num b, Num c) => Num (a, b, c)
> (‘Data.NumInstances.Tuple’)
> ==> Num Int                --                           Num Int
> (‘GHC.Num’)
> ==> Num Float              --                           Num Float
> (‘GHC.Float’)
> ==> Num Rational           -- type Rational = Ratio Integer
> (‘GHC.Real’)
>  =  Num (Ration Integer)   -- Integral a             => Num (Ratio a)
> (‘GHC.Real’)
>   ==> Integral Integer     --                           Integral Integer
> (‘GHC.Real’)
> }}}
>
> ----
>
> Not the same idea but similar. Listing instance resolution that takes
> place in an expression
>
> {{{
> >> :elab (+) @Int
> from: (+) @Int
>   Num Int
> }}}
> {{{
> >> :elab2 comparing (length @[]) <> compare
> from: length @[]
>   Foldable []
>
> from: comparing (length @[])
>   Ord Int
>
> from: comparing (length @[]) <> compare
>   Monoid ([a] -> [a] -> Ordering)
>   ==> Monoid ([a] -> Ordering)
>     ==> Monoid Ordering
> }}}
> {{{
> >> :elab2 ask 'a'
> from: ask 'a'
>   MonadReader Char ((->) m)
>   ==> MonadReader Char ((->) Char)
> }}}
>
> not sure about that last one, or how to visualize them but I think it
> gives the right idea.
>
> Make sure to test it on
> https://jpaykin.github.io/papers/paykin_dissertation_2018.pdf
>
> {{{#!hs
> lam
>   :: (HasLolli exp, KnownNat n,
>       Div_ (Remove n ctx') (Remove n ctx') ~ '[],
>       Fresh (Remove n ctx') ~ n,
>       MergeF (Remove n ctx') '[] ~ Remove n ctx', MergeF ctx' '[] ~ ctx',
>       Lookup ctx' n ~ 'Just a, AddF n a (Remove n ctx') ~ ctx',
>       Div_ ctx' ctx' ~ '[]) =>
>      (Var exp n a -> exp ctx' b) -> exp (Remove n ctx') (a -· b)
> }}}

New description:

 Another GHCi command (#15610), `:elab <constraint>` traces instance
 resolution for `<constraint>`. This is already something people do by hand
 (ticket:10318#comment:6) and would be a great tool for explorers of
 Haskell

 {{{
 >> :elab Monoid (a -> b -> ([c], Sum Int))
 Monoid (a -> b -> ([c], Sum Int))
 ==> Monoid (b -> ([c], Sum Int))
   ==> Monoid ([c], Sum Int)
     ==> Monoid [c]
     ==> Monoid (Sum Int)
       ==> Num Int
 }}}

 If resolving the type class fails, it can pinpoint what caused it to fail

 {{{
 >> data A
 >> :elab Show (A, Int -> Int)
 Show (A, Int -> Int)
 <~bRZsz NO instance~>

 ==> Show A
   <NO instance>
 ==> Show (Int -> Int)
   <NO instance>
 }}}

 A verbose version can explain each step

 {{{
 >> :elab +v Monoid (a -> b -> ([c], Sum Int)
 Monoid (a -> b -> ([c], Sum Int)) -- Monoid b => Monoid (a -> b)
 (‘GHC.Base’)
 ==> Monoid (b -> ([c], Sum Int))  -- Monoid b => Monoid (a -> b)
 (‘GHC.Base’)
   ==> Monoid ([c], Sum Int)       -- Monoid b => Monoid (a -> b)
 (‘GHC.Base’)
     ==> Monoid [c]                --             Monoid [a]
 (‘GHC.Base’)
     ==> Monoid (Sum Int)          -- Num    a => Monoid (Sum a)
 (‘Data.Monoid’)
       ==> Num Int                 --             Num Int
 (‘GHC.Num’)
 }}}

 {{{
 >> :elab +v Num (Int, Float, Rational)
 Num (Int, Float, Rational) --  (Num a, Num b, Num c) => Num (a, b, c)
 (‘Data.NumInstances.Tuple’)
 ==> Num Int                --                           Num Int
 (‘GHC.Num’)
 ==> Num Float              --                           Num Float
 (‘GHC.Float’)
 ==> Num Rational           -- type Rational = Ratio Integer
 (‘GHC.Real’)
  =  Num (Ration Integer)   -- Integral a             => Num (Ratio a)
 (‘GHC.Real’)
   ==> Integral Integer     --                           Integral Integer
 (‘GHC.Real’)
 }}}

 ----

 Not the same idea but similar. Listing instance resolution that takes
 place in an expression

 {{{
 >> :elab (+) @Int
 from: (+) @Int
   Num Int
 }}}
 {{{
 >> :elab2 comparing (length @[]) <> compare
 from: length @[]
   Foldable []

 from: comparing (length @[])
   Ord Int

 from: comparing (length @[]) <> compare
   Monoid ([a] -> [a] -> Ordering)
   ==> Monoid ([a] -> Ordering)
     ==> Monoid Ordering
 }}}
 {{{
 >> :elab2 ask 'a'
 from: ask 'a'
   MonadReader Char ((->) m)
   ==> MonadReader Char ((->) Char)
 }}}

 not sure about that last one, or how to visualize them but I think it
 gives the right idea.

 Make sure to test it on
 https://jpaykin.github.io/papers/paykin_dissertation_2018.pdf

 {{{#!hs
 lam
   :: (HasLolli exp, KnownNat n,
       Div_ (Remove n ctx') (Remove n ctx') ~ '[],
       Fresh (Remove n ctx') ~ n,
       MergeF (Remove n ctx') '[] ~ Remove n ctx', MergeF ctx' '[] ~ ctx',
       Lookup ctx' n ~ 'Just a, AddF n a (Remove n ctx') ~ ctx',
       Div_ ctx' ctx' ~ '[]) =>
      (Var exp n a -> exp ctx' b) -> exp (Remove n ctx') (a -· b)
 }}}

 and
 [https://www.reddit.com/r/haskell/comments/ahu6jp/fun_fact_the_continuation_monad_cont_r_a_has_an/eejuhlq/
 this]

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15613#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler