#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Changes (by johnleo): * version: 8.0.1 => 8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Replying to [comment:5 mpickering]:

It's possible that the panic also happens in 8.0.1 because it is caused by an assertion failure. Assertions are not turned on in the released builds.

Thanks, I didn't know that. Here's an example of a function from Generics which also has strange unicode display behavior, but which does not cause a panic in 8.1: {{{ :t (:*:) (:*:) ∷ ∀ {g ∷ ★ → *} {p} {f ∷ ★ → *}. f p → g p → (:*:) ★ f g p }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

:set -XTypeInType class C a where f :: a b :t f f ∷ ∀ {k} {b ∷ k} {a ∷ k → ★}. C k a ⇒ a b class C a where f :: b a :t f f ∷ ∀ {k} {a ∷ k} {b ∷ k → ★}. C k a ⇒ b a }}} However at 3 variables every combination fails (I've used +v here to

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Info after further investigation. The following both work fine. {{{ prevent deep instantiation, which is where the failure occurs). {{{

class C a where f :: a b c :t +v f f ∷ ∀ {k1} {k2} (a ∷ k1 → k2 → ★). C k1 k2 a ⇒ ∀ (b ∷ k1) (c ∷ k2). a b c class C a where f :: b a c :t +v f f ∷ ∀ {k} (a ∷ k). C k a ⇒ ∀ {k1} (b ∷ k → k1 → ★) (c ∷ k1). b a c class C a where f :: b c a :t +v f f ∷ ∀ {k} (a ∷ k). C k a ⇒ ∀ {k1} (b ∷ k1 → k → ★) (c ∷ k1). b c a }}} All three of these panic without the +v. Note that with no TypeInType everything is fine {{{ class C a where f :: a b c :t f f ∷ ∀ {b} {a ∷ ★ → ★ → ★} {c}. C a ⇒ a b c }}}

The problem seems to be that in the TypeInType case with 3 variables, the quantification of some variables is moving to the right of the class constraint. Variables are instantiated in independent groups, with separate groups before and after the constraint, and here the types after the constraint are referring to kinds defined before the constraint, causing the panic. I will investigate further -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Replying to [comment:9 goldfire]:

Looks to me that you're hot on the case. Let me know if I can be of help.

If you have any insight as to why some of the universally quantified variables are moved past the class constraint in 8.1 that would be very helpful. Was this on purpose to fix some bug (it's not clear to me if the semantics are different or not), or might it just have been an unintended side-effect of some other change? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Replying to [comment:11 goldfire]:

There's clearly something wrong with instantiation here, but the types for the class methods should be the same in 8.0 as in 8.1.

Actually as noted above they are in fact different. In 8.0.1: {{{

class C a where f :: b a c :t f f ∷ ∀ {k} {k1} {a ∷ k} {b ∷ k → k1 → ★} {c ∷ k1}. C k a ⇒ b a c }}}

class C a where f :: b a c :t +v f f ∷ ∀ {k} (a ∷ k). C k a ⇒ ∀ {k1} (b ∷ k → k1 → ★) (c ∷ k1). b a c }}} The bug is then that in 8.1 the `k` referred to by `b` tries to reference

In 8.1: {{{ the kind defined before the class constraint, which is not in scope at that point, causing the panic. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

But you don't have `+v` in 8.0. The type that you're seeing has been instantiated and then regeneralized, so all the variable ordering has been forgotten. I still claim that the internal types assigned to `f` are the same. You just can't ask GHCi for this type in 8.0. You could, though do a `pprTrace` or `traceTc` from `TcExpr.tcInferId` which can print out the uninstantiated type.

In your last sentence: that `k` really ought to be in scope throughout

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Replying to [comment:13 goldfire]: the type. If it's not, there's your bug! OK, I understand. Perhaps it is a bug in 8.0 as well then. The code seems to be instantiating variables in independent groups, in this case the group before the class constraint and then separately the group after the class constraint. If you know a reason for this let me know. Options for fixing it would include doing all the variables together whether they are before or after the constraint, or saving variables from early groups to be in scope for later groups (perhaps the two are essentially equivalent). I'll explore further. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Note that this bug was "fixed" in https://git.haskell.org/ghc.git/commitdiff/f4a14d6c535bdf52b19f441fe185ea13d... (see https://ghc.haskell.org/trac/ghc/ticket/12785) by replacing `substTy` with `substTyUnchecked` in `new_meta_tv_x` (TcMType.hs). See below. Here is my understanding of the problem. The panic happens for example for this call: {{{ :set -XPolyKinds class C a where f :: a b c :type f }}} Unique names have been simplified for readability. The original type (all skolem variables) is the following: {{{ ∀ {kf} {kh} (a9 ∷ kf → kh → ★). C kf kh a9 ⇒ ∀ (ba ∷ kf) (cb ∷ kh). a9 ba cb }}} The outer call to deeply instantiate substitutes `kf -> kj, kh -> kk, a9 -> al` where the new variables are all tau. Theta becomes `C kj kk al` and we call `deeplyinstantiate` now on `∀ (ba ∷ kj) (cb ∷ kk). al ba cb` where it attempts to substitute `ba -> bp, cb -> cq` Substitutions are created by `newMetaTyVars` which is defined as follows. {{{ newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst -- emptyTCvSubst has an empty in-scope set, but that's fine here -- Since the tyvars are freshly made, they cannot possibly be -- captured by any existing for-alls. }}} Note the comment: `kj` and `kk` are free variables in the range of the upcoming substitutions but are not part of the in-scope set. They were however "freshly made" in the outer call. Now `newMetaTyVarX` calls `new_meta_tv_x` which includes this line (before SPJ's change): {{{ kind = substTy subst (tyVarKind tv) }}} Note that `subst` at this point contains the substitutions made prior to the current one, and so is originally empty. So `substTy` succeeds on `ba -> bp` (with kind `kj`), and `bp` and `kj` are added to the in-scope set. However on the second attempt `cb -> cq` (with kind `kk`), since `subst` is now non-empty, `substTy` calls `checkValidSubst` with arguments `subst` and `[kk]`. `checkValidSubst` does two checks, the second of which (`tysColsFVsInScope`) fails. This checks that `kk` is in the in-scope set which consists of `{kj, bp}`, and thus the panic. Although I understand the problem, I don't know the best way to fix it. Certainly retaining `kk` and the others in the in-scope set for the recursive call to `deeplyInstantiate` would be sufficient, but I'm not sure why it's necessary. No real substitution is being done for `kk` at this point, so it is not clear why we need to check the substitution invariant. And even if there was a substitution since the variables are fresh there should no risk of capture during alpha-renaming. While I was investigating this, SPJ made the change mentioned at the top of this note, which is: {{{ kind = substTyUnchecked subst (tyVarKind tv) -- Unchecked because we call newMetaTyVarX from -- tcInstBinderX, which is called from tc_infer_args -- which does not yet take enough trouble to ensure -- the in-scope set is right; e.g. Trac #12785 trips -- if we use substTy here }}} This indicates that there is a more wide-spread problem, so I don't want to make any changes that would break something else. I'm happy to investigate fixing the larger problem, however. In any case I'd appreciate some guidance at this point. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Thank you, that is indeed very helpful. I agree that comment in `newMetaTyVars` is very likely incorrect and the source of bugs. However I believe the panic that occurs in this case is actually a different problem. First note that the actual substitutions of the kinds that results in `∀ (ba ∷ kj) (cb ∷ kk). al ba cb` happens earlier, on the line {{{ ; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho) }}} of `deeplyInstantiate`. Note that the substitution was already unchecked there, likely due to the problem you mention (as well as perhaps other problems). The panic in the line {{{ kind = substTy subst (tyVarKind tv) }}} that happens later seems unrelated to the substitution invariant. At this point the kinds have already been substituted, so it is trying to do the substitution `kk -> kk`, which in fact satisfies the invariant. The code line above is very suspicious to me--I'm not sure why any substitution for the kind is being attempted. Why not just `kind = tyVarKind tv`? If all kinds must be specified before the types that use them (and I assume that is checked somewhere earlier) then the kind substitution must have already been happened. The problem seems to be that `subst` here is the substitution for the type variable, but we pass in the kind variable as the second argument to `substTy` which confuses `checkValidSubst`. This can be seen from the values printed out by the assert (here with the full names). {{{ in_scope InScope {k_a12j b_a12p} tenv [a11a :-> b_a12p[tau:2]] cenv [] tys [k_a12k[tau:2]] cos [] needInScope [a12k :-> k_a12k[tau:2]] }}} The substitution being attempted is `kk -> kk` but `tenv` contains the `ba -> bp` substitution. So in the lines {{{ needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos) `delListFromUFM_Directly` substDomain }}} of `checkValidSubst` the `substDomain` (of `tenv`) is getting removed from `needInScope` but it is the wrong domain--it should be `kk`, not `ba`. Anyway it seems there seem to be a lot of problems with this code, and it's certainly worth going through and cleaning up, but again I'd appreciate some perspective to make sure I'm not breaking more than I fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): It's buried a bit in all the text I wrote above (written when I was still trying to understand the code), but it's the line {{{ = do { (subst, tvs') <- newMetaTyVars tvs }}} of `deeplyInstantiate`, particularly inside the recursive call that happens a few lines down. {{{ ; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho) }}} In the example I give above there are two forall groups. The first works fine and substitutions are made into the second via the `substTyUnchecked`, in particular into the kind variables of the second group. However these kind variables are not part of the the in-scope set when {{{ kind = substTyUnchecked subst (tyVarKind tv) }}} is called in `new_meta_tv_x` of the second, recursive, call of `deeplyInstantiate`, since `newMetaTyVars ` starts with a fresh empty in- scope set, thus the panic I was looking at. As I noted above, the kind variables being substituted into are "fresh" from the outer call and thus there will be no real problem, but it's probably better to pass them in to `newMetaTyVars` as Richard suggests rather than trying to special-case the checking logic, and there may well still be places where not passing in a pre-existing in-scope set does cause a real problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Thank you, everything makes sense except "does not substitute in `rho`". Perhaps I misunderstood something, but it seems it is essential to substitute into `rho` at some point and nowhere else is it done, so if I leave that out the original skolem variables are never replaced with taus and unification fails later on. Indeed I tried this out and it failed: I get the error `No instance for (C k0 k1 a0) arising from a use of ‘f’` when I try to do `:t f` for `class C a where f :: a b c`. If I leave in the substitution for `rho` everything seems to work fine. Note that I keep the unchecked substitutions in `deeply_instantiate` and only revert the one in `new_meta_tv_x` (which was the one causing the bug in the first place), since I'm worried making the other ones checked will cause other problems. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Thanks, that also works, and as you say is semantically cleaner. I did in fact use `newMetaTyVarsX`; in fact I had to write it since it didn't exist, but it is straightforward. {{{ newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Just like newMetaTyVars, but start with an existing substitution. newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst }}} I'll post the code for review in the near future. Note that I haven't handled `tc_infer_args`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by goldfire): Regardless of anything else: do please file a bug about the `tc_infer_args` problem, so that I have something to put in my queue. Otherwise, this seems to be humming nicely to a conclusion. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Changes (by bgamari): * milestone: => 8.2.1 Comment: Thanks John! Is there a bug describing the `tc_infer_args` issue mentioned in comment:26? I'll keep this ticket open until one is opened so we don't lose track of this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by simonpj): I'm not certain, but I thought that `tc_infer_args` was the only caller of `new_meta_tv_x` which didn't establish the in-scope set. There are lots of `substTyUnchecked` which each need individual attention. I suppose a new ticket that enumerated them would be a good thing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12549: Panic on ":t datatypeName" -------------------------------------+------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: Operating System: MacOS X | Architecture: x86_64 | (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11371 #12785 | Differential Rev(s): #12931 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by johnleo): * status: new => closed * resolution: => fixed * related: 11371 12785 => #11371 #12785 #12931 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler