December 2017 - ghc-tickets

[GHC] #14048: Data instances of kind Constraint
by GHC 29 Mar '18

29 Mar '18

#14048: Data instances of kind Constraint -------------------------------------+------------------------------------- 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: #12369 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Continuation of #12369. Allow data instances ending in `Constraint`. This may be a bug but GHC already accepts (something to do with #11715) `data family Bot :: Constraint` but I can't make instances of it. Also fails for `data family Bot :: TYPE IntRep`. I propose letting users take these disparate data types and type classes {{{#!hs data Compose :: (k' -> Type) -> (k -> k') -> (k -> Type) where Compose :: f (g a) -> Compose f g a data Compose2 :: (k' -> (kk -> Type)) -> (k -> k') -> (k -> (kk -> Type)) where Compose2 :: f (g a) b -> Compose2 f g a b -- ComposeC :: (k' -> Constraint) -> (k -> k') -> (k -> Constraint) class f (g a) => ComposeC f g a instance f (g a) => ComposeC f g a -- ComposeC2 :: (k' -> (kk -> Constraint)) -> (k -> k') -> (k -> (kk -> Constraint)) class f (g a) b => ComposeC2 f g a b instance f (g a) b => ComposeC2 f g a b }}} and unify them as instances of a 'data' family indexed by `Type`, `kk -> Type`, `Constraint`, `kk -> Constraint`. (Same can be done for `Data.Functor.Product` and `class (f a, g a) => ProductC f g a`): {{{#!hs data family (·) :: (k' -> k'') -> (k -> k') -> (k -> k'') data instance (f · g) a where Compose :: f (g a) -> (f · g) a data instance (f · g) a b where Compose2 :: f (g a) b -> (f · g) a b instance f (g a) => (f · g) a instance f (g a) b => (f · g) a b }}} ---- TODO Once we have #1311 allow data instances of unlifted types. ---- Fun note: `(·) @(kk -> Type)` is used by [https://gist.github.com/ekmett/48f1b578cadeeaeee7a309ec6933d7ec Kmett] (as `Tensor`) & to motivate [http://i.cs.hku.hk/~bruno/papers/hs2017.pdf quantified class constraints], this should automatically pick the right data instance: {{{#!hs instance (Trans t, Trans t') => Trans (t · t') where lift :: Monad m => m ~> (t · t') m lift = Compose2 . lift @t . lift @t' }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14048> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #14263: typeKind is quadratic
by GHC 29 Mar '18

29 Mar '18

#14263: typeKind is quadratic -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | 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: -------------------------------------+------------------------------------- While pondering Phab:D3998, I realized that any computation of a type's kind should be careful in the presence of nested `AppTy`s. And, to my horror, I realized that GHC's very own `typeKind` isn't! That is, if you have the type `a b c d e`, GHC will take a quadratic (or worse -- haven't benchmarked) amount of time computing its kind. This can be easily fixed by looking for nested `AppTy`s and using `piResultTys`, instead of repeated uses of `piResultTy` (as is currently done). NB: This was not discovered through witnessing poor performance, but it does seem like very low-hanging compiler-performance fruit. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14263> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 9

[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] #14478: Abstract pattern synonyms (for hsig and hs-boot)
by GHC 27 Mar '18

27 Mar '18

#14478: Abstract pattern synonyms (for hsig and hs-boot) -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: backpack | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Most declaration forms (data types, values, type families, etc) support forward declaration in hs-boot/hsig files. However, pattern synonyms do not. This seems like a major omission! Some problems to solve: * The obvious syntax `pattern Foo :: pat_ty` is insufficient to specify whether or not a pattern is bidirectional or unidirectional. How should this be represented syntactically? * What is the interaction with bundling? Should it be possible to export a bundle of abstract pattern synonyms, with the intent that this means an implementation must also have bundled them together * See also #12717; abstract pattern synonym should be implementable with a plain old constructor -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14478> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[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] #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