Broken types in identifiers bound by :print

mentioned in issue #9046 (closed)

changed weight to 5

added Tbug Trac import labels

mentioned in issue #12458 (closed)

mentioned in issue #15299 (closed)

Also reported at #15299 (closed).

closed

Closing as duplicate of #9046 (closed).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

reopened

#9046 (closed) not present in 8.4.3, but there is #12449 (closed).

Trac metadata

Trac field	Value
Resolution	ResolvedDuplicate → Unresolved

Test added in D4921

Trac metadata

Trac field	Value
Test case	- → ghci/scripts/T12449

added GHCi label

added Pnormal label

I don't see the test case mentioned above (D4921…). Also, the behavior changed substantially over time, and now there is no panic in any of the examples above, but the output feels confusing to me:

~$ ghci
GHCi, version 8.10.1: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/artem/.ghci
λ> :print show
show = (_t1::t1)
λ> :t _t1
_t1 :: Show a => a -> String
λ> _t1 "foo"
"\"foo\""
λ> _t1

<interactive>:4:1: error:
    • No instance for (Show (() -> String))
        arising from a use of ‘print’
        (maybe you haven't applied a function to enough arguments?)
    • In a stmt of an interactive GHCi command: print it
λ>

It seems that _t1 simply gets bounded to show. So you wouldn't get a panic ever with it, but the fact that this binding happens feels somewhat confusing to me.

@ulysses4ever Thanks for your comment! Did you ever try with HEAD?

roland@goms:~$ ghchead --interactive
GHCi, version 8.11.0.20200510: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/roland/.ghci
Prelude> :t show
show :: Show a => a -> String
Prelude> :print show
show = (_t1::Show a => a -> String)
Prelude> :t _t1

<interactive>:1:1: error:
    • No instance for (Show a) arising from a use of ‘_t1’
    • In the expression: _t1
Prelude> _t1 "test"

<interactive>:4:5: error:ghc: panic! (the 'impossible' happened)
  (GHC version 8.11.0.20200510:
	No skolem info:
  [a_aIo]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1218:37 in ghc:GHC.Utils.Outputable
        pprPanic, called at compiler/GHC/Tc/Errors.hs:2827:17 in ghc:GHC.Tc.Errors

Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

I recently added some patches in the "no skolem" area. I'll investigate...

I backed out commit 7c0c76fb (MR !2685 (closed)) from HEAD and got the behavior of 8.10.1! MR 2685 fixed #14828 (closed).

@RyanGlScott: Bad news! Should we backout commit 7c0c76fb and re-open #14828 (closed)?

Indeed, there appear to be some lingering bugs remaining. That being said, I'm not really sure that we'd gain much by reverting 7c0c76fb. While the panic in #12449 (comment 273408) would go away, things like :print fmap would start to panic once more. In the end, we'd be exchanging one panic for another.

In order to make an informed decision about what to do next, we first need to agree on what the correct behavior should be with respect to polymorphic types. To make things simpler, let's revisit the original example of :print id. As noted in the original issue, there's something funny about the type of the resulting _t1:

GHCi, version 8.11.0.20200505: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :print id
id = (_t1::a -> a)
λ> :type +v id
id :: forall a. a -> a
λ> :type +v _t1
_t1 :: a -> a

Notice how the type of id is forall a. a -> a. In other words, this should work for any type a. On the other hand, the type of _t1 is a -> a, which is not quantified over a. In other words, a appears to be free in the type of _t1. I don't think this is intended to happen, as it confuses GHC:

λ> _t1 "foo"

<interactive>:4:5: error:ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.11.0.20200505:
        No skolem info:
  [a_aEf]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1218:37 in ghc:GHC.Utils.Outputable
        pprPanic, called at compiler/GHC/Tc/Errors.hs:2827:17 in ghc:GHC.Tc.Errors

That's clearly not good. But what should happen? I can see two possibilities:

Teach GHC not to panic. Instead, treat the a in _t1 :: a -> a as a rigid type variable that is bound at the top-level in the GHCi session. This would mean that _t1 "foo" would be rejected with a type error (something to the effect of "Can't match type a with String").
Change :print id so that instead of giving _t1 the type a -> a, it gives it the type forall a. a -> a. That way, _t1 "foo" will typecheck.

My feeling is that users would probably desire option (2) more than option (1). But then again, I don't use the GHCi debugger much, so I don't feel qualified to be the authority on this. What are your feelings, @RolandSenn?

added debugger label

@RyanGlScott Thanks for your very quick answer! I think, we should do both options:

Teach GHC not to panic.

The panic "No skolem info" only occurs when GHC tries to print an error message. So this panic always hides a (more or less useful) error message. It's very easy to implement and then GHC prints:

Prelude> _t1 "test"

<interactive>:3:5: error:
    • Couldn't match expected type ‘a’ with actual type ‘[Char]’
        ‘a’ is untouchable
          inside the constraints: ()
          bound by the inferred type of it :: String
          at <interactive>:3:1-10
    • In the first argument of ‘_t1’, namely ‘"test"’
      In the expression: _t1 "test"
      In an equation for ‘it’: it = _t1 "test"

Change :print id so that [...] it gives it the type forall a. a -> a.

This seems to be the proper solution.

From the point of view of the user of the GHCi debugger this is an academic problem: show and _t1 are the same. The user can always use the original name (show in this example) instead of the copy (_t1).

From the point of view of the compiler developer it's a little bit different. Things that are the same should behave the same way. And if they don't, this gives a bad impression.

@ulysses4ever Do you want to give it a try?

@RolandSenn I did not plan to, but if you could provide some pointers, I would take a look over the weekend.

@ulysses4ever I didn't want to spoil your weekend...

Ad (1) panic:

The error message is in compiler/GHC/Tc/Errors.hs:mkTyVarEqErr' in the case below the comment Nastiest case. The panic is in the same module in the function getSkolemInfo. Instead of the panic, I would return an empty list. And in the line above, I would return [(RuntimeUnkSkol, tvs)] if any (not all) element is isRuntimeUnkSkol.

Ad (2) add forall a. a -> a.

This is much more difficult! Unfortunately I can give you only very vague and unspecific hints. As :print _t1 gives an reasonable answer, I would compare the evaluation (type checking) of _t1 "str" vs show "str" and see where and why they take different evaluation pathes. You can either start of the beginning of the evaluation or work backwards from the error message / panic form (1).

If you plan to work on this ticket, please assign it to yourself.

I wish you good luck and much fun.

Thanks, @RolandSenn! I think the second option makes more sense. As you said, it probably requires more investigation. Although I may be able to look into it in the future, by no means anyone should hold their breath about it.

I had another look into this. My current state of debugging:

When the user does a :print show, then in compiler/GHC/Runtime/Heap/Inspect.hs:cvObtainTerm at the beginning we have a quant_old_ty@(old_tvs, old_tau) = quantifyType old_ty. Here old_ty is the type of our term show: forall a. Show a => a -> String. The function quantifyType cuts off the forall a.. This forall is never re-added again to the newly created variable _t1.

Hence the above called option (2) would be to re-add this forall a. to _t1.

However, the users-guide says for :print:

If any unevaluated components (thunks) are encountered, then :print binds a fresh variable with a name beginning with _t to each thunk.

Does show have any unevaluated components (thunks)? No, it's' a compiled function, not an unevaluated thunk!

This gives option (3) to fix this issue: :print foo should not bind a new variable, if foo is a function! The output of print show would just be the same as type show: show :: (Show a => a -> String).

assigned to @RolandSenn

I decided to fix this issue with option (2): Re-add the forall constraint at the end of compiler/GHC/Runtime/Heap/Inspect.hs:cvObtainTerm.

Looking at testcase print036 (and others) I got the impression, that option (3) was not the intention of the original authors.

mentioned in issue #19355 (closed)

mentioned in merge request !4988 (closed)

marked this issue as related to #19355 (closed)

In his comment to !4988 (closed) @rae writes:

But the problem is that quantifyType is deeply strange; I doubt that function can ever be used correctly.

After expanding the type synonym for QuantifiedType the function has the type quantifyType :: Type -> ([TyVar], Type).

The fst part of the return value of quantifyType

Using our running example

fmap :: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b

and looking at the output of quantifyType old_ty in compiler/GHC/Runtime/Heap/Inspect.hs we get old_tvs: [f_ayY]. This is clearly wrong, as the free variables a and b are missing.

In the Note [RuntimeUnkTv] @simonpj writes:

Somewhat surprisingly, :print fmap considers the type of fmap to have nested foralls.

Hence in the function quantifyType we should replace tcSplitForAllInvisTyVars by tcSplitNestedSigmaTys. This function uses tcSplitSigmaTy which splits similar to tcSplitForAllInvisTyVars only invisible type variable binders. For our running example we then get: old_tvs: [a_az1, f_ayY, b_az2] which is much better.

The snd part of the return value of quantifyType

In the snd part of the output the forall quantifiers are removed, the comment says: (quantifyType (forall a. a->[b])) returns ([a,b], a -> [b]). This was not always like this. In GHC-7.6.3, notably the release without the error of this ticket, quantifyType had the following code:

quantifyType :: Type -> QuantifiedType
-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
quantifyType ty = (varSetElems (tyVarsOfType ty), ty)

So quantifyType returned the type of the input unmodified in the snd part. This was changed in commit a8ac471d to fix #8557 (closed) to:

quantifyType :: Type -> QuantifiedType
-- Generalize the type: find all free and forall'd tyvars
-- and return them, together with the type inside, which
-- should not be a forall type.
--
-- Thus (quantifyType (forall a. a->[b]))
-- returns ([a,b], a -> [b])

quantifyType ty = (varSetElems (tyVarsOfType rho), rho)
  where
    (_tvs, rho) = tcSplitForAllTys ty

I didn't find any real arguments, why the foralls must be removed. I found: "The returned Type should have no top-level foralls (I believe)" or "with the type inside, which should not be a forall type" or "I believe that my_ty should not have any enclosing foralls,".

When quantifyType returns the unmodified input type, then the reconstructed types calculated by cvObtainTerm and cvReconstructType have again the necessary foralls. The use of the newly binded _t<n> variables no longer produces error messages. Hence, this fixes #12449 (closed). The GHCi and the debugger testcases, including the one for #8557 (closed), still succeed.

mentioned in merge request !5649 (closed)

mentioned in commit 381db265

closed with commit 39020600

mentioned in commit 39020600

To write the Note(s) suggested by @simonpj I had an other look at the uses of the function quantifyType. This function is used in different places, eg:

In the functions cvObtainTerm and cvReconstructType to calculate the new restricted type from the old_ty and the Constructors found in the Closures. Ticket #12449 (closed) shows, that we need the foralls in the snd field of the result of quantifyType.
As a preprocessor for the arguments of the function check2. This function uses tcSplitTyConApp_maybe to peform the soundness check.

The comment for splitTyConApp_maybesays:

This does not split types headed with (=>), as that's not a TyCon in the type-checker.

For our running example :print fmap the versions before !5649 (closed) did:

tcSplitTyConApp_maybe ( forall a b. Functor f => (a -> b) -> f a -> f b )

with result Nothing. (tcSplitForAllInvisTyVars didn't split properly...)

The version of !5649 (closed) does:

tcSplitTyConApp_maybe ( forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b) )

again with result Nothing.

However if we use the tau type created by tcSplitNestedSigmaTys:

tcSplitTyConApp_maybe ( (a -> b) -> f a -> f b) )

we get: Just (FUN, ['Many, LiftedRep, LiftedRep, a -> b, f a -> f b])

I believed !5649 (closed) was correct, as it didn't change the output of check2 for any of the available test cases! But now I think, the function check2 function really needs tau types. However to fix #12449 (closed) the function quantifyType shouldn't remove the foralls!

Conclusion: We cannot use the same function quantifyType in both places!

I'll prepare a new MR that will fix this. Unfortunately I'm not yet able to come up with a test case that shows the above differences to the GHCi user.

reopened

mentioned in merge request !5758 (closed)

mentioned in commit e4ccd987

mentioned in commit 7a05185a

The follow up MR !5758 (closed) landed, so I close this issue.

closed

mentioned in commit 4d98d44d

mentioned in merge request !6108 (closed)

mentioned in commit 01baf74e

mentioned in commit a3c451be

mentioned in issue #17833

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Broken types in identifiers bound by :print

Child items ...

Activity

Broken types in identifiers bound by :print

Relates to

Activity