[GHC] #12921: initTc: unsolved constraints

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: MacOS X Architecture: x86_64 | Type of failure: Compile-time (amd64) | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While working on a small project of mine, GHC panicked with the following error: {{{ lua-types-0.1.0.0: build Preprocessing executable 'lua-types' for lua-types-0.1.0.0... [2 of 3] Compiling Lua.Parser ( src/Lua/Parser.hs, .stack- work/dist/x86_64-osx/Cabal-1.24.1.0/build/lua-types/lua-types- tmp/Lua/Parser.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.0.1.20161117 for x86_64-apple-darwin): initTc: unsolved constraints WC {wc_insol = [W] explist_a3nf :: t_a3ne[tau:1] (CHoleCan: explist) [W] funccall_a4dv :: t_a4du[tau:1] (CHoleCan: funccall)} Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} From a quick google search, it seems like this is a bug in the type checker. I'm not willing nor able to dive any further into the GHC code myself, though. I'll attach the code as it is, before looking for a workaround. I'm using stack, GHC version 8.0.1.20161117 for x86_64-apple-darwin. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 Type of failure: Compile-time | (amd64) crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by jlp): * Attachment "GHCticket12921.tar.gz" added. Bug-producing project folder -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 Type of failure: Compile-time | (amd64) crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I've trimmed the code down to just this: {{{#!hs {-# LANGUAGE OverloadedStrings #-} module LuaParser (stat) where data Parser a data Stat {-# ANN module "HLint: ignore Reduce duplication" #-} stat :: Parser Stat stat = choice [] }}} This triggers this panic on GHC 8.0.2 and HEAD: {{{ $ /opt/ghc/8.0.2/bin/ghci Bug.hs GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling LuaParser ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.0.2 for x86_64-unknown-linux): initTc: unsolved constraints WC {wc_insol = [W] choice_a13R :: t_a13Q[tau:1] (CHoleCan: choice)} Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} But disturbingly, this panic does //not// occur on GHC 8.0.1, so this is a regression. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 Type of failure: Compile-time | (amd64) crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13106 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13106 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints
-------------------------------------+-------------------------------------
Reporter: jlp | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords:
Operating System: MacOS X | Architecture: x86_64
Type of failure: Compile-time | (amd64)
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: #13106 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):
* cc: simonpj (added)
Comment:
Simon's commit 1ef274298978369e2e07b5c43e635a5ca529a0af:
{{{
From 1ef274298978369e2e07b5c43e635a5ca529a0af Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 Type of failure: Compile-time | (amd64) crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13106 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Thanks. I debugged this last night and I know what is going on. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints
-------------------------------------+-------------------------------------
Reporter: jlp | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords:
Operating System: MacOS X | Architecture: x86_64
Type of failure: Compile-time | (amd64)
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: #13106 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 | (amd64) Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T12921 Blocked By: | Blocking: Related Tickets: #13106 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => typecheck/should_fail/T12921 Comment: Merge to 8.0.3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.3 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 | (amd64) Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T12921 Blocked By: | Blocking: Related Tickets: #13106 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: => 8.0.3 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: Operating System: MacOS X | Architecture: x86_64 | (amd64) Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T12921 Blocked By: | Blocking: Related Tickets: #13106 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gnezdo): I hit this problem too. I couldn't quickly locate a prebuilt version of ghc HEAD. Reporting the reproducer here instead. Given this source: {{{ {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} import GHC.TypeLits -- | The floor of log_2(n). type family Log2 n where Log2 1 = 0 Log2 n = Log2 (Div2 n) + 1 -- | The floor of n/2. type family Div2 n where Div2 0 = 0 Div2 1 = 0 Div2 n = Div2 (n - 2) + 1 }}} In ghci I get the following error: {{{ Prelude> Log2 (2 :: GHC.TypeLits.KnownNat) ghc: panic! (the 'impossible' happened) (GHC version 8.0.2 for x86_64-unknown-linux): initTc: unsolved constraints WC {wc_insol = [W] Log2_a1P3 :: t_a1P2[tau:1] (CHoleCan: Log2) [W] Log2_a1Px :: t_a1Pw[tau:1] (CHoleCan: Log2)} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: Operating System: MacOS X | Architecture: x86_64 | (amd64) Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T12921 Blocked By: | Blocking: Related Tickets: #13106 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): gnezdo, I can confirm that your code no longer panics with GHC 8.2: {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Ok, 1 module loaded. λ> Log2 (2 :: GHC.TypeLits.KnownNat) <interactive>:1:1: error: Data constructor not in scope: Log2 :: t0 -> t1 <interactive>:1:12: error: • Expecting one more argument to ‘KnownNat’ Expected a type, but ‘KnownNat’ has kind ‘Nat -> Constraint’ • In an expression type signature: KnownNat In the first argument of ‘Log2’, namely ‘(2 :: KnownNat)’ In the expression: Log2 (2 :: KnownNat) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12921: initTc: unsolved constraints -------------------------------------+------------------------------------- Reporter: jlp | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: Operating System: MacOS X | Architecture: x86_64 | (amd64) Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T12921 Blocked By: | Blocking: Related Tickets: #13106 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gnezdo): I located a binary and after fixing up the code it's working. Thanks! {{{ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} import Data.Proxy import GHC.TypeLits -- | The floor of log_2(n). type family Log2 n where Log2 1 = 0 Log2 n = Log2 (Div2 n) + 1 -- | The floor of n/2. type family Div2 n where Div2 0 = 0 Div2 1 = 0 Div2 n = Div2 (n - 2) + 1 valueOf :: forall (n :: Nat) . (KnownNat n) => Integer valueOf = natVal (Proxy :: Proxy n) }}} {{{ $ ./ghc-install/bin/ghci a.hs GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( a.hs, interpreted ) Ok, 1 module loaded. *Main> :set -XDataKinds *Main> :set -XTypeApplications *Main> valueOf @(Log2 3) 1 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12921#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC