- ghc-tickets - Haskell.org

[GHC] #9277: GHCi panic: Loading temp shared object failed: Symbol not found
by GHC 14 Feb '19

14 Feb '19

#9277: GHCi panic: Loading temp shared object failed: Symbol not found ----------------------------------+--------------------------------- Reporter: mietek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.8.2 Keywords: | Operating System: MacOS X Architecture: x86_64 (amd64) | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9034, #8935 | ----------------------------------+--------------------------------- When given a Objective-C object file referencing a symbol available in a system framework, GHCi panics saying it can't find the symbol the object file relies on. {{{ $ cat >foo.m <<EOF #import <Foundation/Foundation.h> BOOL is_main_thread() { return [NSThread isMainThread]; } EOF }}} {{{ $ clang -c -o foo.o foo.m }}} {{{ $ ghci -v -framework Foundation foo.o GHCi, version 7.8.2: http://www.haskell.org/ghc/ :? for help Glasgow Haskell Compiler, Version 7.8.2, stage 2 booted by GHC version 7.6.3 Using binary package database: /opt/ghc-7.8.2/lib/ghc-7.8.2/package.conf.d/package.cache wired-in package ghc-prim mapped to ghc- prim-0.3.1.0-948744e1f99cc8bcc7c7d3ba60c7c2d8 wired-in package integer-gmp mapped to integer- gmp-0.5.1.0-dc47f6b546fc171f67a7f7d311684a99 wired-in package base mapped to base-4.7.0.0-a333addb6892f3cc2e6baa5ec782bd04 wired-in package rts mapped to builtin_rts wired-in package template-haskell mapped to template- haskell-2.9.0.0-ed6ecfb467e6936688bb20f968f702e1 wired-in package dph-seq not found. wired-in package dph-par not found. Hsc static flags: Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. *** gcc: /usr/bin/gcc -m64 -fno-stack-protector -DTABLES_NEXT_TO_CODE -L/opt/ghc-7.8.2/lib/ghc-7.8.2/base-4.7.0.0 --print-file-name libiconv.dylib Loading package base ... linking ... done. Loading object (static) foo.o ... Created temporary directory: /var/folders/26/0tzj1txn0vb_0061l4z4rsmr0000gn/T/ghc36377_0 *** Linker: /usr/bin/gcc -m64 -fno-stack-protector -DTABLES_NEXT_TO_CODE -m64 -dynamiclib -o /var/folders/26/0tzj1txn0vb_0061l4z4rsmr0000gn/T/ghc36377_0/ghc36377_1.dylib foo.o -undefined dynamic_lookup -single_module -install_name '@rpath/ghc36377_1.dylib' -L/opt/ghc-7.8.2/lib/ghc-7.8.2/base-4.7.0.0 -Wl,-rpath -Wl,/opt/ghc-7.8.2/lib/ghc-7.8.2/base-4.7.0.0 -L/opt/ghc-7.8.2/lib/ghc-7.8.2/integer-gmp-0.5.1.0 -Wl,-rpath -Wl,/opt/ghc-7.8.2/lib/ghc-7.8.2/integer-gmp-0.5.1.0 -L/opt/ghc-7.8.2/lib/ghc-7.8.2/ghc-prim-0.3.1.0 -Wl,-rpath -Wl,/opt/ghc-7.8.2/lib/ghc-7.8.2/ghc-prim-0.3.1.0 -L/opt/ghc-7.8.2/lib/ghc-7.8.2/rts-1.0 -Wl,-rpath -Wl,/opt/ghc-7.8.2/lib/ghc-7.8.2/rts-1.0 -lHSbase-4.7.0.0-ghc7.8.2 -lHSinteger-gmp-0.5.1.0-ghc7.8.2 -lHSghc-prim-0.3.1.0-ghc7.8.2 -liconv *** Deleting temp files: Deleting: /var/folders/26/0tzj1txn0vb_0061l4z4rsmr0000gn/T/ghc36377_0/ghc36377_1.dylib *** Deleting temp dirs: Deleting: /var/folders/26/0tzj1txn0vb_0061l4z4rsmr0000gn/T/ghc36377_0 ghc: panic! (the 'impossible' happened) (GHC version 7.8.2 for x86_64-apple-darwin): Loading temp shared object failed: dlopen(/var/folders/26/0tzj1txn0vb_0061l4z4rsmr0000gn/T/ghc36377_0/ghc36377_1.dylib, 9): Symbol not found: _OBJC_CLASS_$_NSThread Referenced from: /var/folders/26/0tzj1txn0vb_0061l4z4rsmr0000gn/T/ghc36377_0/ghc36377_1.dylib Expected in: flat namespace in /var/folders/26/0tzj1txn0vb_0061l4z4rsmr0000gn/T/ghc36377_0/ghc36377_1.dylib Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} Note omitting `-framework Foundation` makes no difference to the output. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9277> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #15957: Provide warning for when RecordWildCards LHS {..} doesn't bind anything.
by GHC 14 Feb '19

14 Feb '19

#15957: Provide warning for when RecordWildCards LHS {..} doesn't bind anything. -------------------------------------+------------------------------------- Reporter: Fuuzetsu | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.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: -------------------------------------+------------------------------------- Given simple code like {{{#!haskell {-# LANGUAGE RecordWildCards #-} module M (foo) where data D = D { d1 :: Int, d2 :: Int } foo :: D -> Int -> Int foo D{..} x = x + 5 }}} There is no way that I know of to get GHC to warn us that the {{{ D{..} }}} in {{{foo}}} is not binding anything at all. This is very common after refactoring (perhaps {{{foo}}} looked like {{{foo D{..} x = x + d1 + 5}}} before) and would be great to be able to get a warning about. Of course it's not _dead_ code as it still forces {{{D}}} to WHNF but if we're using {{{RecordWildCards}}} syntax then it's probably not what we were going for. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15957> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #15883: GHC panic: newtype F rep = F (forall (a :: TYPE rep). a)
by GHC 14 Feb '19

14 Feb '19

#15883: GHC panic: newtype F rep = F (forall (a :: TYPE rep). a) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.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: -------------------------------------+------------------------------------- {{{#!hs {-# Language RankNTypes #-} {-# Language KindSignatures #-} {-# Language PolyKinds #-} import GHC.Exts newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) }}} {{{ $ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot- ghci /tmp/U.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/U.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): isUnliftedType forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug > }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15883> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #13595: Should ‘coerce’ be levity polymorphic?
by GHC 14 Feb '19

14 Feb '19

#13595: Should ‘coerce’ be levity polymorphic? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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: #13592 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'm not able to write `coerce @Int# @Int#` or `coerce :: Double# -> Double#`, just checking to see if its intentional or not {{{ >>> :set -XTypeApplications >>> :set -XMagicHash >>> import Data.Coerce >>> import GHC.Exts >>>> :t coerce @Int coerce @Int :: Coercible b Int => Int -> b >>> :t coerce @Int# <interactive>:1:1: error: Couldn't match a lifted type with an unlifted type When matching types b :: * Int# :: TYPE 'IntRep <interactive>:1:9: error: • Expecting a lifted type, but ‘Int#’ is unlifted • In the type ‘Int#’ In the expression: coerce @Int# }}} This was needed for #13592. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13595> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

Re: [GHC] #1311: newtypes of unboxed types disallowed - documentation bug and/or feature request
by GHC 14 Feb '19

14 Feb '19

#1311: newtypes of unboxed types disallowed - documentation bug and/or feature request -------------------------------------+------------------------------------- Reporter: Isaac Dupree | Owner: (none) Type: feature request | Status: patch Priority: low | Milestone: ⊥ Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15219 | Differential Rev(s): Phab:D4777, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/364 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: Phab:D4777 => Phab:D4777, https://gitlab.haskell.org/ghc/ghc/merge_requests/364 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/1311#comment:24> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #15219: Implement UnliftedNewtypes proposal
by GHC 14 Feb '19

14 Feb '19

#15219: Implement UnliftedNewtypes proposal -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple UnliftedNewtypes | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The unlifted newtypes proposal is described here: https://github.com/ghc- proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst I am going to be working on it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15219> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #16317: HIE files don't include module import/export information
by GHC 14 Feb '19

14 Feb '19

#16317: HIE files don't include module import/export information -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.6.3 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: -------------------------------------+------------------------------------- HIE files don't record information about import/exports. This blocks implementing LSIF files which need to know about imports/exports. Export information can be read from `tcg_exports`. Import information can be got from the `HscEnv` and looked up using `findImportedModule` I think. Would be good to target this for 8.8 if there is any time remaining. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16317> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #16316: `-package-env=` in OPTIONS_GHC not supported
by GHC 14 Feb '19

14 Feb '19

#16316: `-package-env=` in OPTIONS_GHC not supported -------------------------------------+------------------------------------- Reporter: hvr | Owner: (none) Type: feature | Status: new request | Priority: high | Milestone: Component: Compiler | Version: 8.6.3 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: -------------------------------------+------------------------------------- I just realised we're missing an ingredient in order to support persistent package-environment workflows for standalone scripts: Consider the following use-cases: ---- 1. Script requires package environemnts disabled {{{#!hs #!/usr/bin/env runghc {-# OPTIONS_GHC -package-env=- #-} main = putStrLn "Hello World" }}} ---- 2. User manually maintains a package environment for scripts or teaching exercises (this is a quite common way to teach Haskell which I subscribe to, by letting students interact with ghc and ghci directly instead, and only properly introducing `cabal` lateron when it's actually needed) {{{ cabal v2-install --lib lens lens-aeson --package-env=lets-lens }}} and the scripts shall be using that custom named package environment: {{{#!hs #!/usr/bin/env runghc {-# OPTIONS_GHC -package-env=lets-lens #-} import Control.Lens main = do putStrLn "Hello Lens" -- ...lens using code... }}} ---- Currently both of these use-cases don't work because {{{ $ ghci-8.6.3 Main.hs GHCi, version 8.6.3: http://www.haskell.org/ghc/ :? for help Main.hs:3:16: error: unknown flag in {-# OPTIONS_GHC #-} pragma: -package-env=lets-lens | 3 | {-# OPTIONS_GHC -package-env=lets-lens #-} | ^^^^^^^^^^^^^^^^^^^^^^^^ }}} I do realise that it's tricky to support package-db related commands in `OPTIONS_GHC` but it'd nevertheless be quite important to support this in some way (possibly with some restrictions) in order to properly support the package-env based workflows (NB: the legacy user pkg-db based ones aren't available anymore in future cabal versions -- package-environments have completely replaced the legacy user-pkg db there). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16316> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #16307: gloss-examples' fluid program takes close to an eternity to compile
by GHC 13 Feb '19

13 Feb '19

#16307: gloss-examples' fluid program takes close to an eternity to compile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 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: -------------------------------------+------------------------------------- It has been over ten minutes and 16 GB of residency and `ghc` `master` still hasn't finished. We should investigate this; something seems very wrong. https://github.com/bgamari/gloss/tree/d863394df7b5a9400f2c2fae08fdbb07c91c6… -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16307> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #16310: Program fails with "Impossible case alternative" when optimized
by GHC 12 Feb '19

12 Feb '19

#16310: Program fails with "Impossible case alternative" when optimized -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: Runtime crash Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here's an (unfortunately rather large) program: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Main (main) where import Data.Kind (Type) import Data.Type.Equality ((:~:)(..)) import Unsafe.Coerce (unsafeCoerce) main :: IO () main = print $ traversableComposition @(M1 U1) @() @() @() @U1 @U1 sPureFun sPureFun (SM1 SU1) ----- sPureFun :: forall f a. SApplicative f => Sing (PureSym0 :: a ~> f a) sPureFun = singFun1 @PureSym0 sPure data family Sing (a :: k) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: a ~> b) (x :: a) :: b data (.@#@$$$) :: forall a b c. (b ~> c) -> (a ~> b) -> a ~> c type instance Apply (f .@#@$$$ g) x = Apply f (Apply g x) newtype instance Sing (f :: k1 ~> k2) = SLambda (forall t. Sing t -> Sing (Apply f t)) type SingFunction1 f = forall t. Sing t -> Sing (Apply f t) singFun1 :: forall f. SingFunction1 f -> Sing f singFun1 f = SLambda f type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t) singFun2 :: forall f. SingFunction2 f -> Sing f singFun2 f = SLambda (\x -> singFun1 (f x)) ----- data U1 p = U1 data instance Sing (z :: U1 p) where SU1 :: Sing 'U1 newtype M1 f p = M1 (f p) data instance Sing (z :: M1 f p) where SM1 :: Sing x -> Sing ('M1 x) data M1Sym0 :: forall k (f :: k -> Type) (p :: k). f p ~> M1 f p type instance Apply M1Sym0 x = 'M1 x newtype Compose f g x = Compose (f (g x)) data ComposeSym0 :: forall k1 k2 (f :: k2 -> Type) (g :: k1 -> k2) (x :: k1). f (g x) ~> Compose f g x type instance Apply ComposeSym0 x = 'Compose x data instance Sing (z :: Compose f g a) where SCompose :: Sing x -> Sing ('Compose x) instance (PFunctor f, PFunctor g) => PFunctor (Compose f g) where type Fmap h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x) instance (SFunctor f, SFunctor g) => SFunctor (Compose f g) where sFmap :: forall a b (h :: a ~> b) (x :: Compose f g a). Sing h -> Sing x -> Sing (Fmap h x) sFmap sh (SCompose sx) = SCompose (sFmap (singFun1 @(FmapSym1 h) (sFmap sh)) sx) instance (PApplicative f, PApplicative g) => PApplicative (Compose f g) where type Pure x = 'Compose (Pure (Pure x)) type 'Compose h <*> 'Compose x = 'Compose (Fmap (<*>@#@$) h <*> x) instance (SApplicative f, SApplicative g) => SApplicative (Compose f g) where sPure sx = SCompose (sPure (sPure sx)) SCompose sh %<*> SCompose sx = SCompose (sFmap (singFun2 @(<*>@#@$) (%<*>)) sh %<*> sx) instance PFunctor U1 where type Fmap _ _ = 'U1 instance SFunctor U1 where sFmap _ _ = SU1 instance VFunctor U1 where fmapCompose _ _ SU1 = Refl instance PFunctor f => PFunctor (M1 f) where type Fmap g ('M1 x) = 'M1 (Fmap g x) instance SFunctor f => SFunctor (M1 f) where sFmap sg (SM1 sx) = SM1 (sFmap sg sx) instance VFunctor f => VFunctor (M1 f) where fmapCompose sg sh (SM1 x) | Refl <- fmapCompose sg sh x = Refl instance PApplicative U1 where type Pure _ = 'U1 type _ <*> _ = 'U1 instance SApplicative U1 where sPure _ = SU1 _ %<*> _ = SU1 instance VApplicative U1 where applicativeHomomorphism _ _ = Refl applicativeFmap _ _ = Refl instance PTraversable U1 where type Traverse _ _ = Pure 'U1 instance STraversable U1 where sTraverse _ _ = sPure SU1 instance VTraversable U1 where traversableComposition :: forall p q r (f :: Type -> Type) (g :: Type -> Type) (h :: p ~> f q) (i :: q ~> g r) (x :: U1 p). (VApplicative f, VApplicative g) => Sing h -> Sing i -> Sing x -> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x)) traversableComposition _ si _ | Refl <- applicativeHomomorphism @f sTraverseI sU1q , Refl <- applicativeFmap @f sTraverseI (sPure sU1q) = Refl where sTraverseI :: Sing (TraverseSym1 i :: U1 q ~> g (U1 r)) sTraverseI = singFun1 (sTraverse si) sU1q :: Sing ('U1 :: U1 q) sU1q = SU1 instance PTraversable f => PTraversable (M1 f) where type Traverse g ('M1 x) = Fmap M1Sym0 (Traverse g x) instance STraversable f => STraversable (M1 f) where sTraverse sg (SM1 sx) = sFmap (singFun1 @M1Sym0 SM1) (sTraverse sg sx) instance VTraversable f => VTraversable (M1 f) where traversableComposition :: forall p q r (cf :: Type -> Type) (cg :: Type -> Type) (h :: p ~> cf q) (i :: q ~> cg r) (x :: M1 f p). (VApplicative cf, VApplicative cg) => Sing h -> Sing i -> Sing x -> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x)) traversableComposition sh si (SM1 (sfp :: Sing fp)) | Refl <- traversableComposition sh si sfp , Refl <- fmapCompose @cf (singFun1 @(FmapSym1 M1Sym0) (sFmap sM1Fun)) sTraverseIFun sTraverseHIp , Refl <- -- Fmap (FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i) (Traverse h fp) -- :~: Fmap (TraverseSym1 i .@#@$$$ M1Sym0) (Traverse h fp) Refl @FmapSym0 `apply` funExt @(f q) @(cg (M1 f r)) @(FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i) @(TraverseSym1 i .@#@$$$ M1Sym0) lemma `apply` Refl @(Traverse h fp) , Refl <- fmapCompose @cf sTraverseIFun sM1Fun sTraverseHIp = Refl where lemma :: forall (z :: f q). Sing z -> Fmap M1Sym0 (Traverse i z) :~: Traverse i (Apply M1Sym0 z) lemma _ = Refl sM1Fun :: forall z. Sing (M1Sym0 :: f z ~> M1 f z) sM1Fun = singFun1 SM1 sTraverseHIp :: Sing (Traverse h fp) sTraverseHIp = sTraverse sh sfp sTraverseIFun :: forall hk. STraversable hk => Sing (TraverseSym1 i :: hk q ~> cg (hk r)) sTraverseIFun = singFun1 (sTraverse si) ----- class PFunctor (f :: Type -> Type) where type Fmap (g :: a ~> b) (x :: f a) :: f b data FmapSym0 :: forall f a b. (a ~> b) ~> f a ~> f b data FmapSym1 :: forall f a b. (a ~> b) -> f a ~> f b type instance Apply FmapSym0 f = FmapSym1 f type instance Apply (FmapSym1 f) x = Fmap f x class SFunctor (f :: Type -> Type) where sFmap :: forall a b (g :: a ~> b) (x :: f a). Sing g -> Sing x -> Sing (Fmap g x) class (PFunctor f, SFunctor f) => VFunctor f where fmapCompose :: forall a b c (g :: b ~> c) (h :: a ~> b) (x :: f a). Sing g -> Sing h -> Sing x -> Fmap g (Fmap h x) :~: Fmap (g .@#@$$$ h) x class PFunctor f => PApplicative f where type Pure (x :: a) :: f a type (g :: f (a ~> b)) <*> (x :: f a) :: f b infixl 4 <*> data PureSym0 :: forall (f :: Type -> Type) a. a ~> f a type instance Apply PureSym0 x = Pure x data (<*>@#@$) :: forall (f :: Type -> Type) a b. f (a ~> b) ~> f a ~> f b data (<*>@#@$$) :: forall (f :: Type -> Type) a b. f (a ~> b) -> f a ~> f b type instance Apply (<*>@#@$) f = (<*>@#@$$) f type instance Apply ((<*>@#@$$) f) x = f <*> x class SFunctor f => SApplicative f where sPure :: forall a (x :: a). Sing x -> Sing (Pure x :: f a) (%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a). Sing g -> Sing x -> Sing (g <*> x) class (PApplicative f, SApplicative f, VFunctor f) => VApplicative f where applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a). Sing g -> Sing x -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b) applicativeFmap :: forall a b (g :: a ~> b) (x :: f a). Sing g -> Sing x -> Fmap g x :~: (Pure g <*> x) class PFunctor t => PTraversable t where type Traverse (g :: a ~> f b) (x :: t a) :: f (t b) data TraverseSym1 :: forall t f a b. (a ~> f b) -> t a ~> f (t b) type instance Apply (TraverseSym1 f) x = Traverse f x class SFunctor t => STraversable t where sTraverse :: forall f a b (g :: a ~> f b) (x :: t a). SApplicative f => Sing g -> Sing x -> Sing (Traverse g x) class (PTraversable t, STraversable t, VFunctor t) => VTraversable t where traversableComposition :: forall a b c (f :: Type -> Type) (g :: Type -> Type) (h :: a ~> f b) (i :: b ~> g c) (x :: t a). (VApplicative f, VApplicative g) => Sing h -> Sing i -> Sing x -> Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x)) ----- funExt :: forall a b (f :: a ~> b) (g :: a ~> b). (forall (x :: a). Sing x -> Apply f x :~: Apply g x) -> f :~: g funExt _ = axiom apply :: f :~: g -> a :~: b -> Apply f a :~: Apply g b apply Refl Refl = Refl axiom :: a :~: b axiom = unsafeCoerce Refl }}} When compiled without optimization, this program prints "`Refl`", as you would expect: {{{ $ /opt/ghc/8.6.3/bin/ghc -O0 Bug.hs -fforce-recomp [1 of 1] Compiling Main ( Bug.hs, Bug.o ) Linking Bug ... $ ./Bug Refl }}} However, when compiled with optimizations, it starts failing at runtime! {{{ $ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp [1 of 1] Compiling Main ( Bug.hs, Bug.o ) Linking Bug ... $ ./Bug Bug: Impossible case alternative }}} This behavior can be observed on all versions of GHC from 8.2.2 to HEAD. Interestingly, this program passes `-dcore-lint` on GHC 8.4.4 through HEAD, but on GHC 8.2.2, it fails `-dcore-lint`: {{{ $ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint [1 of 1] Compiling Main ( Bug.hs, Bug.o ) Linking Bug ... $ /opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint [1 of 1] Compiling Main ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Simplifier *** <no location info>: warning: In a case alternative: (Refl cobox_a1UV :: (FmapSym0 :: (TyFun (f1_X2dk b_a2aC ~> g_a2aF (M1 f1_X2dk c_a2aD)) (f_a2aE (f1_X2dk b_a2aC) ~> f_a2aE (g_a2aF (M1 f1_X2dk c_a2aD))) -> *)) ~# (FmapSym0 :: (TyFun (f1_X2dk b_a2aC ~> g_a2aF (M1 f1_X2dk c_a2aD)) (f_a2aE (f1_X2dk b_a2aC) ~> f_a2aE (g_a2aF (M1 f1_X2dk c_a2aD))) -> *))) No alternatives for a case scrutinee in head-normal form: ($WRefl @ Any @ Any) `cast` (((:~:) (UnsafeCo nominal Any (f b ~> g (M1 f c))) (UnsafeCo nominal Any (FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i)) (UnsafeCo nominal Any (TraverseSym1 i .@#@$$$ M1Sym0)))_R :: ((Any :~: Any) :: *) ~R# (((FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i_a2aH) :~: (TraverseSym1 i_a2aH .@#@$$$ M1Sym0)) :: *)) }}} (The full Core Lint error is absolutely enormous, so I'll post it as a separate attachment.) The one thing about this program that might be considered strange is the use of `axiom = unsafeCoerce Refl`. I believe this should be a perfectly safe use of `unsafeCoerce`, but nevertheless, there is always the possibility that GHC is doing something unsightly when optimizing it. As one curiosity, if you mark `axiom` as `NOINLINE`, then the program produces a different result: {{{ $ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint [1 of 1] Compiling Main ( Bug.hs, Bug.o ) Linking Bug ... $ ./Bug }}} The program simply prints a newline, for some odd reason. (It doesn't appear to throw an exception either, since `echo $?` yields `0`.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16310> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8