September 2017 - ghc-tickets

[GHC] #14155: GHC mentions unlifted types out of the blue (to me anyway)
by GHC 29 Mar '18

29 Mar '18

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This one does me 'ead in, I accidentally type `Ran` instead of `Swap` {{{#!hs {-# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #-} import Data.Coerce newtype Ran g h a = Ran (forall b. (a -> g b) -> h b) newtype Swap p f g a where Swap :: p g f a -> Swap p f g a deriving newtype Show class IxPointed m where ireturn :: a -> m i i a instance IxPointed f => IxPointed (Swap f) where ireturn :: forall a i. a -> Swap f i i a ireturn a = Ran (ireturn a) }}} and get this error {{{ $ ghci -ignore-dot-ghci /tmp/bug.hs GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/bug.hs, interpreted ) /tmp/bug.hs:17:15: error: • Couldn't match expected type ‘Swap f i i a’ with actual type ‘Ran g0 h0 a0’ • In the expression: Ran (ireturn a) In an equation for ‘ireturn’: ireturn a = Ran (ireturn a) In the instance declaration for ‘IxPointed (Swap f)’ • Relevant bindings include a :: a (bound at /tmp/bug.hs:17:11) ireturn :: a -> Swap f i i a (bound at /tmp/bug.hs:17:3) | 17 | ireturn a = Ran (ireturn a) | ^^^^^^^^^^^^^^^ /tmp/bug.hs:17:20: error: • Couldn't match a lifted type with an unlifted type Expected type: (a0 -> g0 b) -> h0 b Actual type: (->) (a0 -> g0 b) (a0 -> g0 b) a • In the first argument of ‘Ran’, namely ‘(ireturn a)’ In the expression: Ran (ireturn a) In an equation for ‘ireturn’: ireturn a = Ran (ireturn a) | 17 | ireturn a = Ran (ireturn a) | ^^^^^^^^^ Failed, modules loaded: none. }}} Is GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(->) :: TYPE rep -> TYPE rep' -> Type` -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14155> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #13062: `opt' failed in phase `LLVM Optimiser'. (Exit code: -11)
by GHC 29 Mar '18

29 Mar '18

#13062: `opt' failed in phase `LLVM Optimiser'. (Exit code: -11) -------------------------------------+------------------------------------- Reporter: 2bdkid | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (LLVM) | Keywords: LLVM | Operating System: Linux Optimiser -11 | Architecture: arm | Type of failure: None/Unknown Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While building [https://hackage.haskell.org/package/unicode-transforms] it fails with: {{{ cabal: Entering directory '/tmp/cabal-tmp-7667/unicode-transforms-0.2.0' Configuring unicode-transforms-0.2.0... Building unicode-transforms-0.2.0... Preprocessing library unicode-transforms-0.2.0... [ 1 of 12] Compiling Data.Unicode.Properties.DecompositionsK ( Data/Unicode/Properties/DecompositionsK.hs, dist/build/Data/Unicode/Properties/DecompositionsK.o ) [ 2 of 12] Compiling Data.Unicode.Properties.Decompositions ( Data/Unicode/Properties/Decompositions.hs, dist/build/Data/Unicode/Properties/Decompositions.o ) [ 3 of 12] Compiling Data.Unicode.Properties.DecomposableK ( Data/Unicode/Properties/DecomposableK.hs, dist/build/Data/Unicode/Properties/DecomposableK.o ) `opt' failed in phase `LLVM Optimiser'. (Exit code: -11) cabal: Leaving directory '/tmp/cabal-tmp-7667/unicode-transforms-0.2.0' }}} Other details: {{{ $ ghc --version The Glorious Glasgow Haskell Compilation System, version 8.0.1 $ opt --version LLVM (http://llvm.org/) LLVM version 3.7.1 Optimized build. Default target: armv7l-unknown-linux-gnueabihf Host CPU: (unknown) }}} I already submitted an issue to the package's bug tracker, but it is believed to be a GHC bug: [https://github.com/harendra-kumar/unicode- transforms/issues/10] -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13062> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #14266: AllowAmbiguousTypes doesn't play well with default class methods
by GHC 29 Mar '18

29 Mar '18

#14266: AllowAmbiguousTypes doesn't play well with default class methods -------------------------------------+------------------------------------- Reporter: chris-martin | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This example does compile, {{{ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ExplicitForAll #-} class A t where f :: forall x m. Monoid x => t m -> m f = undefined instance A [] where f = undefined }}} and it seems that the following really ought to be equivalent to it, since all I have done is remove a method definition which is identical to the default: {{{ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ExplicitForAll #-} class A t where f :: forall x m. Monoid x => t m -> m f = undefined instance A [] }}} But instead GHC 8.0.2 gives an error of "Could not deduce (Monoid x0)" on the instance declaration. (I've also posed the same question on stackoverflow: https://stackoverflow.com/q/46350839/402884.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14266> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 19

[GHC] #14208: Performance with -O2 is worse than with -O0 which is worse than runghc
by GHC 28 Mar '18

28 Mar '18

#14208: Performance with -O2 is worse than with -O0 which is worse than runghc -------------------------------------+------------------------------------- Reporter: harendra | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Runtime Unknown/Multiple | performance bug Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In this particular case `-O2` is 2x slower than `-O0` and `-O0` is 2x slower than `runghc`. Please see the github repo: https://github.com /harendra-kumar/ghc-perf to reproduce the issue. Readme file in the repo has instructions to reproduce. The issue seems to occur when the code is placed in a different module. When all the code is in the same module the problem does not occur. In that case `-O2` is faster than `-O0`. However, when the code is split into two modules the performance gets inverted. Also, it does not occur always, when I tried to change the code to make it simpler for repro the problem did not occur. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14208> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 40

[GHC] #12915: cmmImplementSwitchPlans creates duplicate blocks
by GHC 27 Mar '18

27 Mar '18

#12915: cmmImplementSwitchPlans creates duplicate blocks -------------------------------------+------------------------------------- Reporter: alexbiehl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Given this c-- code *after* common block elimination and *before* cmmImplementSwitchPlans: {{{#!hs ... cfzc: _sfh3::P64 = R1; _cfB7::I64 = %MO_UU_Conv_W32_W64(I32[I64[_sfh3::P64 - 1] - 4]); switch [0 .. 20] _cfB7::I64 { case 2 : goto cfAR; case 4 : goto cfAV; case 6 : goto cfAZ; default: goto cfAC; } cfAZ: _sfh6::I64 = I64[_sfh3::P64 + 7]; _sfgp::I64 = 1; goto sfgo; cfAV: _sfh5::I64 = I64[_sfh3::P64 + 7]; _sfgp::I64 = 1; goto sfgo; cfAR: _sfh4::I64 = I64[_sfh3::P64 + 7]; _sfgp::I64 = 1; goto sfgo; sfgo: ... }}} Everything is fine, the blocks cfAZ, cfAV and cfAR are all a little different. But after cmmImplementSwitchPlans the code becomes: {{{#!hs ... cfzc: _sfgl::I64 = I64[Sp + 24]; _sfgn::P64 = P64[Sp + 16]; _cfB7::I64 = %MO_UU_Conv_W32_W64(I32[I64[R1 - 1] - 4]); if (_cfB7::I64 < 5) goto ufBe; else goto ufBg; ufBe: if (_cfB7::I64 < 4) goto ufBf; else goto cfAV; ufBf: if (_cfB7::I64 != 2) goto cfAC; else goto cfAR; cfAR: _sfgp::I64 = 1; goto sfgo; cfAV: _sfgp::I64 = 1; goto sfgo; ufBg: if (_cfB7::I64 != 6) goto cfAC; else goto cfAZ; cfAZ: _sfgp::I64 = 1; goto sfgo; sfgo: ... }}} We can now see that cfAZ, cfAV and cfAR are code duplicates! Now, https://github.com/ghc/ghc/blob/master/compiler/cmm/CmmPipeline.hs#L72 states {{{ ... ----------- Eliminate common blocks ------------------------------------- g <- {-# SCC "elimCommonBlocks" #-} condPass Opt_CmmElimCommonBlocks elimCommonBlocks g Opt_D_dump_cmm_cbe "Post common block elimination" -- Any work storing block Labels must be performed _after_ -- elimCommonBlocks g <- {-# SCC "createSwitchPlans" #-} runUniqSM $ cmmImplementSwitchPlans dflags g dump Opt_D_dump_cmm_switch "Post switch plan" g ... }}} For some reason I don't understand cmmImplementSwitchPlans is run *after* elimCommonBlocks. Although it seems elimCommonBlocks can deal with the constructs introduced in cmmImplementSwitchPlans. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12915> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #13938: Iface type variable out of scope: k1
by GHC 27 Mar '18

27 Mar '18

#13938: Iface type variable out of scope: k1 -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I managed to make GHC spit out an unusual warning when doing some dependent Haskell recently. This issue is reproducible on GHC 8.0.1, 8.0.2, 8.2.1, and HEAD. You'll need these two files: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Eliminator where import Data.Kind (Type) data family Sing (a :: k) data instance Sing (z :: [a]) where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x:xs) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) -- ^ '(->)' | (:~>) -- ^ '(~>)' class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 $(return []) instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). Sing l -> p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs)) -> p l elimList = elimListPoly @(:->) elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). Sing l -> p @@ '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs)) -> p @@ l elimListTyFun = elimListPoly @(:~>) @_ @p elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). FunApp arr => Sing l -> App [a] arr Type p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs)) -> App [a] arr Type p l elimListPoly SNil pNil _ = pNil elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons) }}} {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ListSpec where import Eliminator import Data.Kind import Data.Type.Equality import GHC.TypeLits type family Length (l :: [a]) :: Nat where {} type family Map (f :: a ~> b) (l :: [a]) :: [b] where {} type WhyMapPreservesLength (f :: x ~> y) (l :: [x]) = Length l :~: Length (Map f l) data WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type type instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]). Length l :~: Length (Map f l) mapPreservesLength = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined }}} You'll need to compile the files like this: {{{ $ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c Eliminator.hs $ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c ListSpec.hs ./Eliminator.hi Declaration for elimListTyFun Unfolding of elimListTyFun: Iface type variable out of scope: k2 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13938> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #14038: TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()
by GHC 27 Mar '18

27 Mar '18

#14038: TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: () -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 (Type checker) | Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This file: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Eliminator where import Data.Kind (Type) data family Sing (a :: k) data instance Sing (z :: [a]) where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x:xs) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) -- ^ '(->)' | (:~>) -- ^ '(~>)' class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). Sing l -> p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs)) -> p l elimList = elimListPoly @(:->) elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). Sing l -> p @@ '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs)) -> p @@ l elimListTyFun = elimListPoly @(:~>) @_ @p elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). FunApp arr => Sing l -> App [a] arr Type p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs)) -> App [a] arr Type p l elimListPoly SNil pNil _ = pNil elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons) }}} Typechecks in GHC 8.2.1 without issue, but fails in GHC HEAD: {{{ $ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Eliminator ( Bug.hs, interpreted ) Bug.hs:59:12: error: • Couldn't match type ‘p0’ with ‘p’ because type variables ‘a1’, ‘p’ would escape their scope These (rigid, skolem) type variables are bound by the type signature for: elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]). Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l at Bug.hs:(54,1)-(58,15) Expected type: Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l Actual type: Sing l -> App [a1] (':->) * p0 '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> App [a1] (':->) * p0 xs -> App [a1] (':->) * p0 (x : xs)) -> App [a1] (':->) * p0 l • In the expression: elimListPoly @(:->) In an equation for ‘elimList’: elimList = elimListPoly @(:->) • Relevant bindings include elimList :: Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l (bound at Bug.hs:59:1) | 59 | elimList = elimListPoly @(:->) | ^^^^^^^^^^^^^^^^^^^ Bug.hs:59:12: error: • Couldn't match type ‘p0’ with ‘p’ ‘p0’ is untouchable inside the constraints: () bound by a type expected by the context: forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> App [a1] (':->) * p0 xs -> App [a1] (':->) * p0 (x : xs) at Bug.hs:59:12-30 ‘p’ is a rigid type variable bound by the type signature for: elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]). Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l at Bug.hs:(54,1)-(58,15) Expected type: Sing x -> Sing xs -> App [a1] (':->) * p0 xs -> App [a1] (':->) * p0 (x : xs) Actual type: Sing x -> Sing xs -> p xs -> p (x : xs) • In the expression: elimListPoly @(:->) In an equation for ‘elimList’: elimList = elimListPoly @(:->) • Relevant bindings include elimList :: Sing l -> p '[] -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> p xs -> p (x : xs)) -> p l (bound at Bug.hs:59:1) | 59 | elimList = elimListPoly @(:->) | ^^^^^^^^^^^^^^^^^^^ }}} A workaround is to explicitly apply `p` with `TypeApplications` in line 59: {{{#!hs elimList = elimListPoly @(:->) @_ @p }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14038> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15

[GHC] #13910: Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)
by GHC 27 Mar '18

27 Mar '18

#13910: Inlining a definition causes GHC to panic (repSplitTyConApp_maybe) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: #13877 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here is a program which I believe //should// typecheck: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Type.Equality data family Sing (a :: k) class SingKind k where type Demote k = (r :: *) | r -> k fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k data SomeSing k where SomeSing :: Sing (a :: k) -> SomeSing k withSomeSing :: forall k r . SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r withSomeSing x f = case toSing x of SomeSing x' -> f x' data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) | (:~>) class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 $(return []) instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 data instance Sing (z :: a :~: b) where SRefl :: Sing Refl instance SingKind (a :~: b) where type Demote (a :~: b) = a :~: b fromSing SRefl = Refl toSing Refl = SomeSing SRefl (~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type). Sing r -> p @@ Refl -> p @@ r (~>:~:) SRefl pRefl = pRefl type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr) (y :: t) (e :: from :~: y) = App t arr Type p y data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr) :: forall (y :: t). from :~: y ~> Type type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x = WhyReplacePoly arr from p y x replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type). p from -> from :~: to -> p to replace = replacePoly @(:->) replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type). p @@ from -> from :~: to -> p @@ to replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t) (p :: (t -?> Type) arr). FunApp arr => App t arr Type p from -> from :~: to -> App t arr Type p to replacePoly from eq = withSomeSing eq $ \(singEq :: Sing r) -> (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t) = App t arr Type f a -> App t arr Type f z data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) :: t ~> Type type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr) (a :: t) (b :: t). FunApp arr => a :~: b -> App t arr Type f a -> App t arr Type f b leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t). a :~: b -> f a -> f b leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id -- The line above is what you get if you inline the definition of leibnizPoly. -- It causes a panic, however. -- -- An equivalent implementation is commented out below, which does *not* -- cause GHC to panic. -- -- leibniz = leibnizPoly @(:->) leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t). a :~: b -> f @@ a -> f @@ b leibnizTyFun = leibnizPoly @(:~>) @_ @f }}} GHC 8.2.1 and HEAD panic on the definition of `leibniz`, however: {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.2.0.20170623 for x86_64-unknown-linux): repSplitTyConApp_maybe (f_a5vT[sk:2] |> Sym (Trans (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N)) (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2] (f_a5vT[sk:2] |> Sym (Trans (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N)) (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2] k2_a5l0 Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} Interestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give the panic from #13877: {{{ $ /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 Bug ( Bug.hs, interpreted ) Bug.hs:134:64: error:ghc: panic! (the 'impossible' happened) (GHC version 8.0.2 for x86_64-unknown-linux): No skolem info: k2_a4KV Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13910> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #13643: Core lint error with TypeInType and TypeFamilyDependencies
by GHC 27 Mar '18

27 Mar '18

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple InjectiveFamilies, TypeInType | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: 12102 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In the code {{{#!hs {-# Language TypeFamilyDependencies #-} {-# Language RankNTypes #-} {-# Language KindSignatures #-} {-# Language DataKinds #-} {-# Language TypeInType #-} {-# Language GADTs #-} import Data.Kind (Type) data Code = I type family Interp (a :: Code) = (res :: Type) | res -> a where Interp I = Bool data T :: forall a. Interp a -> Type where MkNat :: T False instance Show (T a) where show _ = "MkNat" main = do print MkNat }}} but add `{-# Options_GHC -dcore-lint #-}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13643> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #14024: typechecker tests T13594 T13822 tc269 failing in devel2 flavour
by GHC 27 Mar '18

27 Mar '18

#14024: typechecker tests T13594 T13822 tc269 failing in devel2 flavour -------------------------------------+------------------------------------- Reporter: duog | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Test Suite | Version: 8.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The tests T13594 T13822 tc269 are failing for me with BuildFlavour=devel2. They pass with BuildFlavour=validate. I have had a brief look to see if I could fix, but this is beyond my current capabilities. There is a comment in tc269.hs saying that it doesn't typecheck, however that looks to be out of date? test output pasted below: {{{ =====> tc269(normal) 1 of 3 [0, 0, 0] cd "./typecheck/should_compile/tc269.run" && "/home/doug/ghc- dev/devel2/inplace/bin/ghc-stage2" -c tc269.hs -dcore-lint -dcmm-lint -no- user-package-db -rtsopts -fno-warn-missed-specialisations -fshow-warning- groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno-debug- output -fno-warn-incomplete-patterns Compile failed (exit code 1) errors were: ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170723 for x86_64-unknown-linux): ASSERT failed! in_scope InScope {k_aSm} tenv [aRJ :-> k_aSm[sk:2]] tenvFVs [aSg :-> k_aSg[tau:1], aSm :-> k_aSm[sk:2]] cenv [] cenvFVs [] tys [k_aRJ[sk:1] -> *] cos [] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1188:22 in ghc:Outputable assertPprPanic, called at compiler/types/TyCoRep.hs:2089:56 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:2122:29 in ghc:TyCoRep substTy, called at compiler/typecheck/TcCanonical.hs:673:36 in ghc:TcCanonical Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1186:5 in ghc:Outputable assertPprPanic, called at compiler/types/TyCoRep.hs:2089:56 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:2122:29 in ghc:TyCoRep substTy, called at compiler/typecheck/TcCanonical.hs:673:36 in ghc:TcCanonical Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug *** unexpected failure for tc269(normal) =====> T13594(normal) 2 of 3 [0, 1, 0] cd "./typecheck/should_compile/T13594.run" && "/home/doug/ghc- dev/devel2/inplace/bin/ghc-stage2" -c T13594.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn-missed-specialisations -fshow- warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno- debug-output -fno-warn-incomplete-patterns Compile failed (exit code 1) errors were: ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170723 for x86_64-unknown-linux): ASSERT failed! {$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#), !x_a1o5 = (1, 2)} [x] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1188:22 in ghc:Outputable assertPprPanic, called at compiler/deSugar/DsBinds.hs:89:71 in ghc:DsBinds Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1186:5 in ghc:Outputable assertPprPanic, called at compiler/deSugar/DsBinds.hs:89:71 in ghc:DsBinds Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug *** unexpected failure for T13594(normal) =====> T13822(normal) 3 of 3 [0, 2, 0] cd "./typecheck/should_compile/T13822.run" && "/home/doug/ghc- dev/devel2/inplace/bin/ghc-stage2" -c T13822.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn-missed-specialisations -fshow- warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno- debug-output -fno-warn-incomplete-patterns Compile failed (exit code 1) errors were: ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170723 for x86_64-unknown-linux): ASSERT failed! Bad coercion hole {a1bG}: (I (x_a19g |> Sym (Ty (Sym cobox))_N) |> D:R:IK[0]) (I (x_a19g |> Sym (Ty (Sym cobox))_N) |> D:R:IK[0]) nominal <(I (x_a19g |> Sym (Ty (Sym cobox))_N) |> D:R:IK[0])>_N I (x_a19g[ssk:3] |> Sym (Ty (Sym cobox))_N) I (x_a19g[ssk:3] |> Sym (Ty (Sym cobox))_N) nominal Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1188:22 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcMType.hs:304:105 in ghc:TcMType Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1186:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcMType.hs:304:105 in ghc:TcMType Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug *** unexpected failure for T13822(normal) Unexpected results from: TEST="T13594 T13822 tc269" }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14024> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 9