[GHC] #12444: Regression: panic! on inaccessible code with constraint
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Running the following program with ghci-8.0.1: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Prove where data Nat = Zero | Succ Nat data SNat (n :: Nat) where SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n) type family (:+:) (a :: Nat) (b :: Nat) :: Nat where m :+: Zero = m m :+: (Succ n) = Succ (m :+: n) sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m) => SNat m -> SNat n -> SNat (m :+: n) sadd SZero n = n }}} -ddump-tc-trace shows: {{{ ... dischargeFmv s_a9qV[fuv:4] = t_a9qW[tau:5] (1 kicked out) doTopReactFunEq (occurs) old_ev: [D] _ :: ((n1_a9qu[sk] :+: 'Succ s_a9qV[fuv:4]) :: Nat) GHC.Prim.~# (s_a9qV[fuv:4] :: Nat)ghc: panic! (the 'impossible' happened) (GHC version 8.0.1 for x86_64-unknown-linux): ctEvCoercion [D] _ :: (t_a9qW[tau:5] :: Nat) ~# ('Succ (n1_a9qu[sk] :+: s_a9qV[fuv:4]) :: Nat) Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} It is rightly rejected by ghci-7.10.2: {{{ Prove.hs:42:6: Couldn't match type ‘'Succ n1’ with ‘'Zero’ Inaccessible code in a pattern with constructor SZero :: SNat 'Zero, in an equation for ‘sadd’ In the pattern: SZero In an equation for ‘sadd’: sadd SZero n = n Failed, modules loaded: none. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I spent some time investigating. Here's a smaller test case. This program, closely related to the original, makes the constraint solver loop: {{{ data Nat = Zero | Succ Nat data SNat (n :: Nat) type family (:+:) (a :: Nat) (b :: Nat) :: Nat where m :+: Zero = m m :+: (Succ n) = Succ (m :+: n) foo :: SNat (Succ c) -> SNat b -> SNat (Succ (c :+: b)) foo _ x = x }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here’s a slightly simpler example {{{ type instance F (Succ x) = Succ (F x) [W] alpha ~ Succ (F alpha) }}} Solving the constraint goes like this: {{{ Flatten: [W] alpha ~ Succ fuv (CTyVarEq) [W] F alpha ~ fuv (CFunEqCan) Unify alpha := Succ fuv; there’s no occurs check here; and substitute in the other constraint [W] F (Succ fuv) ~ fuv (CFunEqCan) Now we can fire the rule (hooray?) [W] Succ (F fuv) ~ fuv }}} Normally we’d declare at this point that we have figured out what `fuv` is, so we call `dischargeFmv` to update it in place. But we don’t want to unify `fuv := Succ (F fuv)` because that’s makes an infinite type. So instead we turn the fuv into an ordinary unification variable beta, thus `fuv := beta`. So now we have {{{ [W] Succ (F beta) ~ beta }}} And lo, that’s exactly what we started with, so the whole process iterates. This is terrible. It’s a kind of occurs-check loop, but it goes via function call. If we didn’t do flattening we’d have `[W] alpha ~ Succ (F alpha)`, which is an occurs check, so we would not substitute for alpha. Instead we put such occurs-check equalities aside in the “insoluble”. But we do flatten! Of course this example isn’t soluble, but this variant is: {{{ type instance F (Succ a) = Zero [W] alpha ~ Succ (F alpha) }}} Now if we flatten, unify alpha we get {{{ [W] F (Succ fuv) ~ fuv }}} Now fire the rule, and we get {{{ Zero ~ fuv }}} Which is a fine solution. However I would not be too bothered if we didn’t find it. So what should we do? Its bad bad bad for the solver to diverge: note that the type family instance for `F` is perfectly nice. I wasted an entire evening thinking about and trying several ideas, none of which worked. One possibility I didn’t try is to beef up the “occurs check” so that when seeing if `a ~ ty` has an occurs check, we unflatten on-the-fly to see if `a` occurs. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Related: #12526 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash | Test Case: Blocked By: | Blocking: Related Tickets: #12526 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * related: => #12526 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash | Test Case: Blocked By: | Blocking: Related Tickets: #12526 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"1eec1f21268af907f59b5d5c071a9a25de7369c7/ghc" 1eec1f21/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="1eec1f21268af907f59b5d5c071a9a25de7369c7" Another major constraint-solver refactoring This patch takes further my refactoring of the constraint solver, which I've been doing over the last couple of months in consultation with Richard. It fixes a number of tricky bugs that made the constraint solver actually go into a loop, including Trac #12526 Trac #12444 Trac #12538 The main changes are these * Flatten unification variables (fmvs/fuvs) appear on the LHS of a tvar/tyvar equality; thus fmv ~ alpha and not alpha ~ fmv See Note [Put flatten unification variables on the left] in TcUnify. This is implemented by TcUnify.swapOverTyVars. * Don't reduce a "loopy" CFunEqCan where the fsk appears on the LHS: F t1 .. tn ~ fsk where 'fsk' is free in t1..tn. See Note [FunEq occurs-check principle] in TcInteract This neatly stops some infinite loops that people reported; and it allows us to delete some crufty code in reduce_top_fun_eq. And it appears to be no loss whatsoever. As well as fixing loops, ContextStack2 and T5837 both terminate when they didn't before. * Previously we generated "derived shadow" constraints from Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly generate a derived shadow from the same Wanted. A big change in this patch is to have two kinds of Wanteds: [WD] behaves like a pair of a Wanted and a Derived [W] behaves like a Wanted only See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh field of a Wanted. This turned out to be a lot simpler. A [WD] gets split into a [W] and a [D] in TcSMonad.maybeEmitShaodow. See TcSMonad Note [The improvement story and derived shadows] * Rather than have a separate inert_model in the InertCans, I've put the derived equalities back into inert_eqs. We weren't gaining anything from a separate field. * Previously we had a mode for the constraint solver in which it would more aggressively solve Derived constraints; it was used for simplifying the context of a 'deriving' clause, or a 'default' delcaration, for example. But the complexity wasn't worth it; now I just make proper Wanted constraints. See TcMType.cloneWC * Don't generate injectivity improvement for Givens; see Note [No FunEq improvement for Givens] in TcInteract * solveSimpleWanteds leaves the insolubles in-place rather than returning them. Simpler. I also did lots of work on comments, including fixing Trac #12821. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash | polykinds/T12444 Blocked By: | Blocking: Related Tickets: #12526 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => polykinds/T12444 * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12444: Regression: panic! on inaccessible code with constraint -------------------------------------+------------------------------------- Reporter: zilinc | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash | polykinds/T12444 Blocked By: | Blocking: Related Tickets: #12526 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"c48595eef2bca6d91ec0a649839f8066f269e6a4/ghc" c48595ee/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="c48595eef2bca6d91ec0a649839f8066f269e6a4" Never apply worker/wrapper to DFuns While fixing Trac #12444 I found an occasion on which we applied worker/wrapper to a DFunId. This is bad: it destroys the magic DFunUnfolding. This patch is a minor refactoring that stops this corner case happening, and tidies up the code a bit too. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC