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

#15613: GHCi command, tracing steps of instance resolution for Constraint or expression -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature | Status: new request | Priority: lowest | Milestone: Component: GHCi | Version: Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #15610 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Another GHCi command (#15610) to trace the process of instance resolution for a constraint. This is already something people do by hand (ticket:10318#comment:6) and would be a great tool for explorers of Haskell This constraint ultimately boils down to lists being monoids and `Int` being a number {{{
: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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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) to trace the process of instance resolution for a constraint. This is already something people do by hand (ticket:10318#comment:6) and would be a great tool for explorers of Haskell
This constraint ultimately boils down to lists being monoids and `Int` being a number
{{{
: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.
New description: Another GHCi command (#15610) to trace the process of instance resolution for a constraint. This is already something people do by hand (ticket:10318#comment:6) and would be a great tool for explorers of Haskell This constraint ultimately boils down to lists being monoids and `Int` being a number {{{
: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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by monoidal): See also #9622. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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) to trace the process of instance resolution for a constraint. This is already something people do by hand (ticket:10318#comment:6) and would be a great tool for explorers of Haskell
This constraint ultimately boils down to lists being monoids and `Int` being a number
{{{
: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.
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 This constraint ultimately boils down to lists being monoids and `Int` being a number {{{
: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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:2 monoidal]: Yeah this is almost identical to monoidal's #9622. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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
This constraint ultimately boils down to lists being monoids and `Int` being a number
{{{
: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.
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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Reminder to self: display some kind of name, show how the final dictionary is constructed {{{ $fSemigroup-> :: forall b a. Semigroup b => Semigroup (a -> b) $fSemigroupBool :: Semigroup Any }}} and information about Given/Wanted (stuff listed by `-ddump-tc-trace`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by simonpj): All this would be cool, but it'd take some work to implement. Plus, remember it's a tree: a goal may lead to multiple sub-goals... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack):
Plus, remember it's a tree: a goal may lead to multiple sub-goals...
Yes. Should I make a GHC proposal or is it minimal enough to decide here? I started implementing it: Where do I tap into the current machinery and how best to pass the tree back? It took me a while to be able to find the class being solved, by using `mkClassPred clas tys` in definitions like [https://hackage.haskell.org/package/ghc-8.4.3/docs/src/TcInteract.html#runSo... runSolverPipeline], [https://hackage.haskell.org/package/ghc-8.4.3/docs/src/InstEnv.html#memberIn... matchInstEnv] .. {{{#!hs run_pipeline ((stg_name,stg):stgs) (ContinueWith ct) = do { traceTcS ("runStage " ++ stg_name ++ " {") (text "workitem = " <+> ppr ct) ; res <- stg ct ; let current :: PredType current = mkClassPred clas tys ; traceTcS ("end stage " ++ stg_name ++ " }") empty ; run_pipeline stgs res } }}} and then calling `hscTcExpr` from ''UI''. I'm sure there is a better way but that's how I got started -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by simonpj): I think you might want something more like `simplifyDefault` or `solveWanteds`, both exported by `TcSimplify`. Mostly these functions are used ''within'' the typechecker, but the pattern match overlap checker uses the constraint solver in `Check.tyOracle`. A significant factor is whether you want any "givens"; that is, do you want to explain why a constraint fails to be solved under a GADT match, or in a function with a given context. Once you get deeper into the constraint solver, solving one step of each individual constraint, you need the `TcS` monad, which holds the inert set... I'm not sure you want to get into that. Better to tell the constraint solver to try to solve, and see what is left over: it'll return (a) any unsolved constraints and (b) evidence bindings that amount to a specification of the exact proof that it came up with; i.e. the tree you want to display. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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.
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) }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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_m... this] -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15613#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC