January 2018 - ghc-tickets

[GHC] #11503: TypeError woes (incl. pattern match checker)
by GHC 01 Mar '19

01 Mar '19

#11503: TypeError woes (incl. pattern match checker) -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.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: -------------------------------------+------------------------------------- When I say {{{ {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, UndecidableInstances #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Bug where import GHC.TypeLits import GHC.Exts ( Constraint ) type family NotInt a where NotInt Int = TypeError (Text "That's Int, silly.") NotInt _ = (() :: Constraint) data T a where MkT1 :: a -> T a MkT2 :: NotInt a => T a foo :: T Int -> Int foo (MkT1 x) = x }}} I get {{{ Bug.hs:19:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: MkT2 }}} But I shouldn't. Even worse, perhaps, GHC accepts my pattern-match against `MkT2` if I add it. If I change the `TypeError` to `False ~ True`, I get the correct behavior. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11503> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #14109: GHC matches -- as a varsym when lexing a qvarsym
by GHC 28 Feb '19

28 Feb '19

#14109: GHC matches -- as a varsym when lexing a qvarsym -------------------------------------+------------------------------------- Reporter: glguy | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Parser) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Other Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC seems only to exclude the line comment marker `--` when lexing a varsym and not a qvarsym. This can be observed in the following code {{{ module Demo where x Demo.-- y = (x,y) }}} Generating this surprising error message {{{ /Users/emertens/Desktop/Demo.hs:3:3: error: Qualified name in binding position: Demo.-- }}} and excludes this definition perhaps? {{{ example f = Just.-- comment f }}} Which might either have lexed as `Just` `.` `-- comment`, or it might have lexed as `Just.-` `-`, but it probably shouldn't be the case that it's a qvarsym. At a minimum, the Haskell Report specifically excludes `--` from the varsym rule, so it can't support the qvarsym rule match that it is now. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14109> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[GHC] #9121: Presence of dyn_o files not checked? upon recompilation
by GHC 28 Feb '19

28 Feb '19

#9121: Presence of dyn_o files not checked? upon recompilation ------------------------------------+------------------------------------- Reporter: andreas.abel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Build System | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- When I interrupt a compilation (initiated with cabal), and then recompile (with cabal), it can happen that gcc fails with missing .dyn_o file. I have "shared:True" in my .cabal/config file. [I can of course do cabal clean to work around, but since a full recompilation is about 10 min, I try to avoid this.] time cabal install --disable-library-profiling --disable-documentation Resolving dependencies... In order, the following will be installed: Agda-2.3.3 (latest: 2.3.2.2) (reinstall) Warning: Note that reinstalls are always dangerous. Continuing anyway... Configuring Agda-2.3.3... Building Agda-2.3.3... Preprocessing library Agda-2.3.3... [116 of 273] Compiling Agda.TypeChecking.Monad.Base[boot] ( src/full/Agda/TypeChecking/Monad/Base.hs-boot, dist/build/Agda/TypeChecking/Monad/Base.o-boot ) ... [239 of 273] Compiling Agda.TypeChecking.Conversion ( src/full/Agda/TypeChecking/Conversion.hs, dist/build/Agda/TypeChecking/Conversion.o ) [Agda.Syntax.Translation.InternalToAbstract changed] ^Cmake: *** [install-bin] Interrupt time cabal install --disable-library-profiling --disable-documentation Resolving dependencies... In order, the following will be installed: Agda-2.3.3 (latest: 2.3.2.2) (reinstall) Warning: Note that reinstalls are always dangerous. Continuing anyway... Configuring Agda-2.3.3... Building Agda-2.3.3... Preprocessing library Agda-2.3.3... [116 of 273] Compiling Agda.TypeChecking.Monad.Base[boot] ( src/full/Agda/TypeChecking/Monad/Base.hs-boot, dist/build/Agda/TypeChecking/Monad/Base.o-boot ) ... [273 of 273] Compiling Agda.Main ( src/full/Agda/Main.hs, dist/build/Agda/Main.o ) [Agda.Compiler.Epic.Compiler changed] gcc: error: dist/build/Agda/TypeChecking/Conversion.dyn_o: No such file or directory Failed to install Agda-2.3.3 cabal: Error: some packages failed to install: Agda-2.3.3 failed during the building phase. The exception was: ExitFailure 1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9121> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #14419: Check kinds for ambiguity
by GHC 27 Feb '19

27 Feb '19

#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | 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: -------------------------------------+------------------------------------- GHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected: {{{#!hs type family F a data T :: F a -> Type }}} `T`'s kind is ambiguous, and any occurrence of `T` will be rejected. Instead of rejecting usage sites, let's just reject the definition site. This check would be disabled by `AllowAmbiguousTypes`. Happily, I think the implementation should be easy, and that the current algorithm to check for ambiguous types should work for kinds, too. After all, types and kinds are the same these days. This was inspired by #14203, but no need to read that ticket to understand this one. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14419> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #13408: Consider inferring a higher-rank kind for type synonyms
by GHC 27 Feb '19

27 Feb '19

#13408: Consider inferring a higher-rank kind for type synonyms -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example: {{{#!hs f :: (forall a. a -> a -> a) -> Int f z = z 0 1 g = f }}} `g` gets an inferred type equal to `f`'s. However, this fails at the type level: {{{#!hs type F (z :: forall a. a -> a -> a) = z 0 1 type G = F }}} If anything is strange here, it's that the term-level definition is accepted. GHC should not be in the business of inferring higher-rank types. But there is an exception for definitions comprising one non- recursive equation. This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted. This is spun off from #13399, but is not tightly coupled to that ticket. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13408> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #10170: Find versioned versions of LLVM tools
by GHC 25 Feb '19

25 Feb '19

#10170: Find versioned versions of LLVM tools -------------------------------------+------------------------------------- Reporter: erikd | Owner: erikd Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.11 (LLVM) | Operating System: Unknown/Multiple Keywords: | Type of failure: None/Unknown Architecture: | Blocked By: Unknown/Multiple | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Since it has become more widely know that the LLVM developers often make breaking changes to the IR language between releases, some Linu distributions (eg Debain and hence Ubuntu) have started doing multi- version LLVM installs. For instance on Debian, the llvm-3.6 programs are installed in `/usr/lib/llvm-3.6/bin` as `llc` and `opt`. I propose that the `configure.ac` and `aclocal.m4` configuration goop be modified to look for `llc` and `opt` in these versioned `/usr/lib/llvm-X.Y` locations. I'm also willing to do the hard yards on implementing this if people think its a good idea. This can be seen as a step along the way to more stringent LLVM versioning requirements. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10170> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 19

[GHC] #14198: Inconsistent treatment of implicitly bound kind variables as free-floating
by GHC 21 Feb '19

21 Feb '19

#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #7873 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- (Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.) This program is accepted: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo = MkFoo (forall a. Proxy a) }}} There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`: {{{ λ> :i Foo data Foo = forall k. MkFoo (forall (a :: k). Proxy a) }}} This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But to make things stranger, it you write out the kind of `a` explicitly: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo2 = MkFoo2 (forall (a :: k). Proxy a) }}} Then GHC will reject it: {{{ Bug.hs:7:1: error: Kind variable ‘k’ is implicitly bound in data type ‘Foo2’, but does not appear as the kind of any of its type variables. Perhaps you meant to bind it (with TypeInType) explicitly somewhere? | 7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} So GHC's treatment is inconsistent. What should GHC do? We could: * Have both be an error. * Have both be accepted, and implicitly quantify `k` as an existential type variable * Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is: {{{#!hs MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo }}} * Something else. When you try a similar trick with type synonyms: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy type Foo3 = forall a. Proxy a }}} Instead of generalizing the kind of `a`, its kind will default to `Any`: {{{ λ> :i Foo3 type Foo3 = forall (a :: GHC.Types.Any). Proxy a }}} Would that be an appropriate trick for data types as well? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14198> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #12564: Type family in type pattern kind
by GHC 20 Feb '19

20 Feb '19

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell: {{{#!haskell {-# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #-} import Data.Kind data N = Z | S N type family Len (xs :: [a]) :: N where Len '[] = Z Len (_ ': xs) = S (Len xs) data Fin :: N -> Type where FZ :: Fin (S n) FS :: Fin n -> Fin (S n) type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where At (x ': _) FZ = x At (_ ': xs) (FS i) = At xs i }}} It fails to compile with this error: {{{ FinAt.hs:16:3: error: • Illegal type synonym family application in instance: 'FZ • In the equations for closed type family ‘At’ In the type family declaration for ‘At’ }}} That's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application. I tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce: {{{#!haskell x :: At '[Bool] FZ x = True }}} results in {{{ FinAt.hs:20:5: error: • Couldn't match expected type ‘At * ((':) * Bool ('[] *)) ('FZ 'Z)’ with actual type ‘Bool’ • In the expression: True In an equation for ‘x’: x = True }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12564> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 16

[GHC] #13971: Misleading "Kind mis-match on LHS of default declaration" error
by GHC 19 Feb '19

19 Feb '19

#13971: Misleading "Kind mis-match on LHS of default declaration" error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This program fails to typecheck, unsurprisingly: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Bug where class C a where type T a :: k type T a = Int }}} But the error message it gives threw me for a loop initially: {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:7:3: error: • Kind mis-match on LHS of default declaration for ‘T’ • In the default type instance declaration for ‘T’ In the class declaration for ‘C’ | 7 | type T a = Int | ^^^^^^^^^^^^^^ Failed, 0 modules loaded. }}} The LHS of the default declaration is perfectly fine - the real source of the error is the RHS! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13971> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[GHC] #13706: ghci messages like "Ok, modules loaded: ..." are impractical for large sets of modules
by GHC 18 Feb '19

18 Feb '19

#13706: ghci messages like "Ok, modules loaded: ..." are impractical for large sets of modules -------------------------------------+------------------------------------- Reporter: j.waldmann | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: GHCi | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Ghci (in the default config) wants to show me all the modules that are currently loaded. If I have a great many of these (think: hundreds) then this is impractical, because I have to scroll back to see what actually interests me (output of last command). I can change the prompt (`:set prompt "> "`), but I don't see how to switch off the display of all module names in `:r` command. I have to scroll back (several screenfulls) to even find out whether the reload was successful, since the status (OK/Failed) is at the very beginning - and the reason for the Failure is before that. Cf. https://mail.haskell.org/pipermail/haskell-cafe/2017-May/126983.html (but there was no reaction) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13706> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2