February 2018 - ghc-tickets

[GHC] #14496: Invoking GHC 8.2.1 executable anywhere results in access violation on Windows 10
by GHC 27 Mar '18

27 Mar '18

#14496: Invoking GHC 8.2.1 executable anywhere results in access violation on Windows 10 -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Windows Architecture: | Type of failure: GHC doesn't work Unknown/Multiple | at all Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This apparently started to happen somewhat recently, as I've been able to run GHC 8.2.1 on Windows before. (Perhaps it was a recent update that changed things?) In any case, any attempt to run GHC or GHCi 8.2.1 immediately results in an access violation, and always at the same memory location: {{{ $ ghc --version The Glorious Glasgow Haskell Compilation System, version 8.2.1 $ ghc Access violation in generated code when reading 000000001170399e $ ghci WARNING: GHCi invoked via 'ghci.exe' in MinTTY consoles (e.g., Cygwin or MSYS) doesn't handle Ctrl-C well; use the 'ghcii.sh' shell wrapper instead GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Access violation in generated code when reading 000000001170399e }}} Strangely enough, GHC 8.0.2 and older do not suffer from this issue, just 8.2.1. In case it's useful, here's the `strace` output: {{{ $ strace ghc Access violation in generated code when reading 000000001170399e create_child: ghc --- Process 10324 created --- Process 10324 loaded C:\Windows\System32\ntdll.dll at 00007ffa31280000 --- Process 10324 loaded C:\Windows\System32\kernel32.dll at 00007ffa31170000 --- Process 10324 loaded C:\Windows\System32\KernelBase.dll at 00007ffa2dd40000 --- Process 10324 loaded C:\Windows\System32\apphelp.dll at 00007ffa2b500000 --- Process 10324 loaded C:\Windows\System32\AcLayers.dll at 00007ffa03630000 --- Process 10324 loaded C:\Windows\System32\msvcrt.dll at 00007ffa30ab0000 --- Process 10324 loaded C:\Windows\System32\user32.dll at 00007ffa2e850000 --- Process 10324 loaded C:\Windows\System32\win32u.dll at 00007ffa2dba0000 --- Process 10324 loaded C:\Windows\System32\gdi32.dll at 00007ffa2ec30000 --- Process 10324 loaded C:\Windows\System32\gdi32full.dll at 00007ffa2da00000 --- Process 10324 loaded C:\Windows\System32\msvcp_win.dll at 00007ffa2d960000 --- Process 10324 loaded C:\Windows\System32\ucrtbase.dll at 00007ffa2dbc0000 --- Process 10324 loaded C:\Windows\System32\shlwapi.dll at 00007ffa2e7f0000 --- Process 10324 loaded C:\Windows\System32\combase.dll at 00007ffa30e50000 --- Process 10324 loaded C:\Windows\System32\rpcrt4.dll at 00007ffa2e9e0000 --- Process 10324 loaded C:\Windows\System32\bcryptprimitives.dll at 00007ffa2dcc0000 --- Process 10324 loaded C:\Windows\System32\sfc.dll at 0000000180000000 --- Process 10324 loaded C:\Windows\System32\winspool.drv at 00007ffa1db00000 --- Process 10324 loaded C:\Windows\System32\IPHLPAPI.DLL at 00007ffa2cb90000 --- Process 10324 loaded C:\Windows\System32\bcrypt.dll at 00007ffa2d0d0000 --- Process 10324 loaded C:\Windows\System32\sfc_os.dll at 00007ffa1c2e0000 --- Process 10324 loaded C:\Windows\System32\imm32.dll at 00007ffa31220000 --- Process 10324 loaded C:\Windows\System32\shell32.dll at 00007ffa2ef80000 --- Process 10324 loaded C:\Windows\System32\cfgmgr32.dll at 00007ffa2e700000 --- Process 10324 thread 3948 created --- Process 10324 loaded C:\Windows\System32\SHCore.dll at 00007ffa30cf0000 --- Process 10324 loaded C:\Windows\System32\windows.storage.dll at 00007ffa2dfb0000 --- Process 10324 loaded C:\Windows\System32\advapi32.dll at 00007ffa30da0000 --- Process 10324 loaded C:\Windows\System32\sechost.dll at 00007ffa2eb00000 --- Process 10324 thread 4764 created --- Process 10324 loaded C:\Windows\System32\kernel.appcore.dll at 00007ffa2d660000 --- Process 10324 loaded C:\Windows\System32\powrprof.dll at 00007ffa2d5f0000 --- Process 10324 loaded C:\Windows\System32\profapi.dll at 00007ffa2d5d0000 --- Process 10324 thread 3852 created --- Process 10324 loaded C:\Windows\System32\wsock32.dll at 00007ffa1c2b0000 --- Process 10324 loaded C:\Windows\System32\ws2_32.dll at 00007ffa2ef10000 --- Process 10324 loaded C:\Windows\System32\ws2_32.dll at 0000000000150000 --- Process 10324 unloaded DLL at 0000000000150000 --- Process 10324 thread 4872 created --- Process 10324 thread 5780 created --- Process 10324 thread 8360 created --- Process 10324, exception c0000005 at 00007ffa3129c12e --- Process 10324 thread 8360 exited with status 0x1 --- Process 10324 thread 5780 exited with status 0x1 --- Process 10324 thread 4872 exited with status 0x1 --- Process 10324 thread 3852 exited with status 0x1 --- Process 10324 thread 4764 exited with status 0x1 --- Process 10324 thread 3948 exited with status 0x1 --- Process 10324 exited with status 0x1 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14496> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[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] #14720: GHC 8.4.1-alpha regression with TypeInType
by GHC 26 Mar '18

26 Mar '18

#14720: GHC 8.4.1-alpha regression with TypeInType -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.4.1-alpha1 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC 8.2.2 is able to typecheck this code: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module SGenerics where import Data.Kind (Type) import Data.Type.Equality ((:~:)(..), sym, trans) import Data.Void data family Sing (z :: k) class Generic (a :: Type) where type Rep a :: Type from :: a -> Rep a to :: Rep a -> a class PGeneric (a :: Type) where type PFrom (x :: a) :: Rep a type PTo (x :: Rep a) :: a class SGeneric k where sFrom :: forall (a :: k). Sing a -> Sing (PFrom a) sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k) class (PGeneric k, SGeneric k) => VGeneric k where sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a data Decision a = Proved a | Disproved (a -> Void) class SDecide k where (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k)) => Sing a -> Sing b -> Decision (a :~: b) s1 %~ s2 = case sFrom s1 %~ sFrom s2 of Proved (Refl :: PFrom a :~: PFrom b) -> case (sTof s1, sTof s2) of (Refl, Refl) -> Proved Refl Disproved contra -> Disproved (\Refl -> contra Refl) }}} But GHC 8.4.1-alpha2 cannot: {{{ $ /opt/ghc/8.4.1/bin/ghc Bug.hs [1 of 1] Compiling SGenerics ( Bug.hs, Bug.o ) Bug.hs:44:52: error: • Could not deduce: PFrom a ~ PFrom a from the context: b ~ a bound by a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in a lambda abstraction at Bug.hs:44:37-40 Expected type: PFrom a :~: PFrom b Actual type: PFrom a :~: PFrom a NB: ‘PFrom’ is a non-injective type family • In the first argument of ‘contra’, namely ‘Refl’ In the expression: contra Refl In the first argument of ‘Disproved’, namely ‘(\ Refl -> contra Refl)’ • Relevant bindings include contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15) s2 :: Sing b (bound at Bug.hs:40:9) s1 :: Sing a (bound at Bug.hs:40:3) (%~) :: Sing a -> Sing b -> Decision (a :~: b) (bound at Bug.hs:40:3) | 44 | Disproved contra -> Disproved (\Refl -> contra Refl) | ^^^^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14720> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #14441: GHC HEAD regression involving type families in kinds
by GHC 26 Mar '18

26 Mar '18

#14441: GHC HEAD regression involving type families in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: #13790 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In GHC 8.2.1, this file typechecks: {{{#!hs {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind type family Demote (k :: Type) :: Type type family DemoteX (a :: k) :: Demote k data Prox (a :: k) = P type instance Demote (Prox (a :: k)) = Prox (DemoteX a) $(return []) type instance DemoteX P = P }}} (Note that the `$(return [])` line is essential, as it works around #13790.) However, on GHC HEAD, this now fails: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:27: error: • Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’ • In the type ‘P’ In the type instance declaration for ‘DemoteX’ | 15 | type instance DemoteX P = P | ^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14441> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

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

26 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] #14556: Core Lint error: Ill-kinded result in coercion
by GHC 26 Mar '18

26 Mar '18

#14556: Core Lint error: Ill-kinded result in coercion -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #14554 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-} import Data.Kind import Data.Proxy data Fn a b where IdSym :: Fn Type Type type family (@@) (f::Fn k k') (a::k)::k' where IdSym @@ a = a data KIND = X | FNARR KIND KIND data TY :: KIND -> Type where ID :: TY (FNARR X X) FNAPP :: TY (FNARR k k') -> TY k -> TY k' data TyRep (kind::KIND) :: TY kind -> Type where TID :: TyRep (FNARR X X) ID TFnApp :: TyRep (FNARR k k') f -> TyRep k a -> TyRep k' (FNAPP f a) type family IK (kind::KIND) :: Type where IK X = Type IK (FNARR k k') = Fn (IK k) (IK k') type family IT (ty::TY kind) :: IK kind where IT ID = IdSym IT (FNAPP f x) = IT f @@ IT x zero :: TyRep X a -> IT a zero = undefined }}} which gives Core lint error when run with `ghci -ignore-dot-ghci -dcore- lint` (8.3.20171122) attached. It compiles fine with {{{#!hs zero :: TyRep X a -> IT a zero = zero }}} but fails with `zero = let x = x in x`. See #14554. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14556> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

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

26 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

[GHC] #14846: Renamer hangs (because of -XInstanceSigs?)
by GHC 26 Mar '18

26 Mar '18

#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: InstanceSigs | Operating System: Unknown/Multiple TypeInType | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs #-} import Data.Kind import Data.Proxy type Cat ob = ob -> ob -> Type data Struct :: (k -> Constraint) -> Type where S :: Proxy (a::k) -> Struct (cls::k -> Constraint) type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls) data AStruct :: Struct cls -> Type where AStruct :: cls a => AStruct (Structured a cls) class StructI (structured::Struct (cls :: k -> Constraint)) where struct :: AStruct structured instance (Structured xx cls ~ structured, cls xx) => StructI structured where struct :: AStruct (Structured xx cls) struct = AStruct data Hom :: Cat k -> Cat (Struct cls) where class Category (cat::Cat ob) where i :: StructI a => ríki a a instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where i :: forall a. StructI a => Hom ríki a a i = case struct :: AStruct (Structured a cls) of }}} Running on 8.2.1 and 8.5.20180105 both loop until interrupted {{{ $ ghci -ignore-dot-ghci 199.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 199.hs, interpreted ) ^CInterrupted. > > }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14846> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10