[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
#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
participants (1)
-
GHC