February 2018 - ghc-tickets

[GHC] #10954: Add class/context information to typed hole relevant bindings
by GHC 02 Apr '18

02 Apr '18

#10954: Add class/context information to typed hole relevant bindings -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #9479 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC's typed hole messages don't currently include any known context information for relevant bindings. For example: {{{#!hs bar :: a ~ b => a -> b -> Int bar x y = _ }}} gets me {{{ Found hole ‘_’ with type: Int Relevant bindings include y :: b (bound at <interactive>:8:42) x :: a (bound at <interactive>:8:40) bar :: a -> b -> Int (bound at <interactive>:8:36) In the expression: _ In an equation for ‘bar’: bar x y = _ }}} The types `a` and `b` are not unified, and the `a ~ b` constraint is not shown. {{{#!hs foo :: Show a => a -> Int foo x = _ }}} gets me {{{ Found hole ‘_’ with type: Int Relevant bindings include x :: a (bound at <interactive>:4:36) foo :: a -> Int (bound at <interactive>:4:32) In the expression: _ In an equation for ‘foo’: foo x = _ }}} The `Show` constraint is lost. === What I want === I'd like context information for all type variables in known bindings, so I can see all the pieces available to help me fill in the hole. === Related ticket === In #9479, Dominique Devriese wants to see any constraints ''on'' an ambiguously-typed hole. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10954> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #10267: Add support for typed holes in Template Haskell
by GHC 02 Apr '18

02 Apr '18

#10267: Add support for typed holes in Template Haskell -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.10.1 Component: Template | Operating System: Unknown/Multiple Haskell | Type of failure: None/Unknown Keywords: | Blocked By: Architecture: | Related Tickets: Unknown/Multiple | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- I want to be able to work with typed holes using Template Haskell. These are currently rejected: {{{#!hs [d| i :: a -> a i x = _ |] }}} {{{ Expression form not (yet) handled by Template Haskell _ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10267> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #14749: T13822 fails
by GHC 02 Apr '18

02 Apr '18

#14749: T13822 fails -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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: -------------------------------------+------------------------------------- Consider this cut-down T13822 {{{ {-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-} module T13822 where import Data.Kind data KIND = STAR | KIND :> KIND data Ty :: KIND -> Type where TMaybe :: Ty (STAR :> STAR) TApp :: Ty (a :> b) -> (Ty a -> Ty b) type family IK (k :: KIND) = (res :: Type) where IK STAR = Type IK (a:>b) = IK a -> IK b type family I (t :: Ty k) = (res :: IK k) where I TMaybe = Maybe I (TApp f a) = (I f) (I a) data TyRep (k :: KIND) (t :: Ty k) where TyMaybe :: TyRep (STAR:>STAR) TMaybe TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x) zero :: TyRep STAR a -> I a zero x = case x of TyApp TyMaybe _ -> Nothing }}} With a stage-1 compiler with DEBUG enabled, this program yields a Lint error in all recent versions of GHC. (NB: Lint, not an assertion failure.) With stage-2 it succeeds, and passes Lint. But an apparently unrelated patch makes it fail Lint even in stage 2. I conclude that the bug is not in the unrelated patch; it is somehow there all along. I'll mark T13822 as expect-broken; you can re-enable it when this ticket is fixed. The Lint error is pretty obscure {{{ *** Core Lint errors : in result of Desugar (before optimization) *** <no location info>: warning: [in body of letrec with binders co_a10u :: (f_a10g :: Ty (a_a10f ':> 'STAR)) ~# (('TMaybe |> (Ty (Sym co_a10r ':> <'STAR>_N)_N)_N) :: Ty (a_a10f ':> 'STAR))] Kind application error in coercion ‘(Maybe (Sym (Coh <I (x_a10h |> Sym (Ty (Sym co_a10r))_N)>_N (D:R:IK[0]) ; Coh <(I (x_a10h |> Sym (Ty (Sym co_a10r))_N) |> D:R:IK[0])>_N (Sym (D:R:IK[0]))) ; Coh <I (x_a10h |> Sym (Ty (Sym co_a10r))_N)>_N (D:R:IK[0])))_N’ Function kind = * -> * Arg kinds = [(I (x_a10h |> Sym (Ty (Sym co_a10r))_N), IK 'STAR)] Fun: * (I (x_a10h |> Sym (Ty (Sym co_a10r))_N), IK 'STAR) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14749> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #14066: Skolem escape at the kind level
by GHC 02 Apr '18

02 Apr '18

#14066: Skolem escape at the kind level -------------------------------------+------------------------------------- Reporter: simonpj | 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: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This program should be rejected {{{ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE KindSignatures #-} module Foo2 where import Data.Kind ( Type ) import Data.Type.Equality import Data.Proxy import GHC.Exts data SameKind :: k -> k -> Type f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b g = undefined in () }}} But * 8.0 rejects it, with an unhelpful message * 8.2 accepts it, and the result satisfies Core Lint * HEAD accepts it, and produces a Core Lint Error -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14066> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #10822: GHC inconsistently handles \\?\ for long paths on Windows
by GHC 31 Mar '18

31 Mar '18

#10822: GHC inconsistently handles \\?\ for long paths on Windows -------------------------------------+------------------------------------- Reporter: snoyberg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Windows Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- To demonstrate what I mean first: {{{ >ghc-pkg init \\?\c:\Users\michael\Desktop\some-pkg-db >dir \\?\c:\Users\Michael\Desktop\some-pkg-db Volume in drive \\?\c: is Windows8_OS Volume Serial Number is CEF7-874D Directory of \\?\c:\Users\Michael\Desktop\some-pkg-db 09/01/2015 09:38 AM <DIR> . 09/01/2015 09:38 AM <DIR> .. 09/01/2015 09:38 AM 40 package.cache 1 File(s) 40 bytes 2 Dir(s) 5,907,509,248 bytes free >ghc -package-db \\?\c:\Users\Michael\Desktop\some-pkg-db ghc: can't find a package database at \\?\c:\Users\Michael\Desktop\some- pkg-db }}} The problem: on Windows by default, paths are limited to 260 characters, which can become a real problem in practice when dealing with the standard library path hierarchy the Cabal library uses and any package with a decent name length. This was a real problem in practice, see: https://github.com/haskell/cabal/issues/2502 Windows has a workaround for this: you can prefix an absolute path with \\?\, see: https://msdn.microsoft.com/en- us/library/windows/desktop/aa365247%28v=vs.85%29.aspx#maxpath It would be very useful if such paths worked with GHC, but currently they do not. I don't yet know how deep the problem is. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10822> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>)
by GHC 31 Mar '18

31 Mar '18

#14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This code works fine: {{{#!hs {-# Language TypeOperators, RankNTypes, KindSignatures, GADTs, DataKinds, MultiParamTypeClasses, FlexibleInstances, ConstraintKinds, ScopedTypeVariables #-} import Data.Kind -- 'constraints' machinery data Dict c where Dict :: c => Dict c newtype a :- b = Sub (a => Dict b) -- entailment -- 'singletons' machinery data SBool :: Bool -> Type where SFalse :: SBool 'False STrue :: SBool 'True class SBoolI (bool::Bool) where sbool :: SBool bool instance SBoolI 'False where sbool = SFalse instance SBoolI 'True where sbool = STrue -- VVV Example VVV class Funny (b::Bool) (b'::Bool) instance Funny 'False b' instance Funny 'True 'True instance Funny 'True 'False proof :: forall b b'. (SBoolI b, SBoolI b') :- Funny b b' proof = Sub (case (sbool :: SBool b, sbool :: SBool b') of (SFalse, _) -> Dict (STrue, SFalse) -> Dict (STrue, STrue) -> Dict) -- ^^^ Example ^^^ }}} What I'm interested in is the entailment: Singletons for `b` and `b'` entail `Funny b b'`. This is witnessed by `proof`. Given that we have a branch for `-XQuantifiedConstraints`, it is tantalizing to convert this into an implication constraint `(SBoolI b, SBoolI b') => Funny b b'`. Is such a thing sensible (wrt coherence) and if so is it at all possible to do this on WIPT2893? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14822> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #14728: Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?
by GHC 30 Mar '18

30 Mar '18

#14728: Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: deriving, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In Phab:D2636, I implemented this ability to use `GeneralizedNewtypeDeriving` to derive instances of type classes with associated type families. At the time, I thought the implementation was a no-brainer, but now I'm starting to have second thoughts. To explain what I mean, consider this program: {{{#!hs {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Functor.Identity import Data.Kind class C (a :: Type) where type T a (x :: a) :: Type instance C () where type T () '() = Bool deriving instance C (Identity a) }}} Quite to my surprise, this typechecks. Let's consult `-ddump-deriv` to figure out what code is being generated: {{{ $ /opt/ghc/8.2.2/bin/ghci Bug.hs -ddump-deriv GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance Bug.C (Data.Functor.Identity.Identity a) where Derived type family instances: type Bug.T (Data.Functor.Identity.Identity a1_a1M3) x_a1M5 = Bug.T a1_a1M3 x_a1M5 }}} Hm... OK. Since GHC was able to generate this code, surely we should be able to write it ourselves, right? {{{#!hs {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Functor.Identity import Data.Kind class C (a :: Type) where type T a (x :: a) :: Type instance C () where type T () '() = Bool -- deriving instance C (Identity a) instance C (Identity a) where type T (Identity a) x = T a x }}} {{{ $ /opt/ghc/8.2.2/bin/ghci Bug.hs GHCi, version 8.2.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:19:31: error: • Occurs check: cannot construct the infinite kind: a ~ Identity a • In the second argument of ‘T’, namely ‘x’ In the type ‘T a x’ In the type instance declaration for ‘T’ | 19 | type T (Identity a) x = T a x | ^ }}} Uh-oh. GHC gets quite angry when we try to type this in ourselves, which isn't a good sign. This raises the question: just what is GHC doing in the previous version of the program? I tried to answer that question by seeing if `T (Identity a) x` could ever reduce: {{{#!hs {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Functor.Identity import Data.Kind class C (a :: Type) where type T a (x :: a) :: Type instance C () where type T () '() = Bool deriving instance C (Identity a) f :: T (Identity ()) ('Identity '()) f = True }}} And lo and behold, you get: {{{ $ /opt/ghc/8.2.2/bin/ghci Bug.hs GHCi, version 8.2.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:19:5: error: • Couldn't match type ‘T () ('Identity '())’ with ‘Bool’ Expected type: T (Identity ()) ('Identity '()) Actual type: Bool • In the expression: True In an equation for ‘f’: f = True | 19 | f = True | ^^^^ }}} It appears that `T (Identity ()) ('Identity '())` reduced to `T () ('Identity '())`. At that point, it becomes stuck. (Perhaps it's for the best that it's the case—if `T () ('Identity '())` managed to reduce, who knows what kind of mischief GHC could get itself into.) But all of this leads me to wonder: is something broken in the implementation of this feature, or is `GeneralizedNewtypeDeriving` simply not sound with respect to associated type families? I certainly hope that it's not the latter, as it's quite a useful feature. But at the same time, it's hard to reconcile that usefulness with the strange behavior above. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14728> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 16

[GHC] #12442: Pure unifier usually doesn't need to unify kinds
by GHC 30 Mar '18

30 Mar '18

#12442: Pure unifier usually doesn't need to unify kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new 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: -------------------------------------+------------------------------------- The pure unifier (in `types/Unify.hs`) is used to match up instances with actual types. Since GHC 8, it matches up the kinds with the types in a separate pass. But this is often wasteful, and sometimes downright wrong. It's wasteful because most invocations of the unifier on a list of types pass in well-kinded arguments to some type constructor. Because the kinds of type constructors are closed, if we process the list left-to-right, we will always unify the kinds of later arguments before we get to them. So we shouldn't take another pass on the kinds. It's wrong because it's conceivable for the kind to include a type family application, and using a type family application as a template in the pure unifier is very silly, indeed. I cam across this while trying to translate Idris's algebraic effects library to Haskell. My reduced test case is attached. Patch on the way. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12442> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #12176: Failure of bidirectional type inference at the kind level
by GHC 30 Mar '18

30 Mar '18

#12176: Failure of bidirectional type inference at the kind level -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new 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: -------------------------------------+------------------------------------- I'm feeling particularly sadistic towards GHC at the moment, and so I fed it this: {{{ import Data.Kind data Proxy :: forall k. k -> Type where MkProxy :: forall k (a :: k). Proxy a data X where MkX :: forall (k :: Type) (a :: k). Proxy a -> X type Expr = (MkX :: forall (a :: Bool). Proxy a -> X) type family Foo (x :: forall (a :: k). Proxy a -> X) where Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k) }}} Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi telling me the following (with `-fprint-explicit-kinds`): {{{ λ> :i Foo type family Foo k (x :: forall (a :: k). Proxy k a -> X) :: Proxy * k where [k] Foo k ('MkX k) = 'MkProxy * k }}} That is, I wished to extract the kind parameter to `MkK`, matching against a partially-applied `MkX`, and GHC understood that intention. However, sadly, writing `Foo Expr` produces {{{ • Expected kind ‘forall (a :: k0). Proxy k0 a -> X’, but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’ • In the first argument of ‘Foo’, namely ‘Expr’ In the type ‘Foo Expr’ In the type family declaration for ‘XXX’ }}} For some reason, `Expr` is getting instantiated when it shouldn't be. Perhaps there's a simpler test case demonstrating the bug, but I feel so gleeful that this chicanery is accepted at all that I wanted to post. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12176> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #9406: unexpected failure for T7837(profasm)
by GHC 29 Mar '18

29 Mar '18

#9406: unexpected failure for T7837(profasm) -------------------------------------+------------------------------------- Reporter: jrp | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Test Suite | Version: 7.8.3 Keywords: T7837 | Operating System: MacOS X Architecture: x86_64 (amd64) | Type of failure: Incorrect Difficulty: Unknown | result at runtime Blocked By: | Test Case: T7837 Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- This may be a test suite configuration error as the normal case works. When run with an llvm-perf build of the HEAD, I get: {{{ =====> T7837(normal) 1395 of 4068 [0, 0, 0] cd ./indexed-types/should_compile && '/Users/jrp/Projects/haskell/ghc/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-db -rtsopts -fno-ghci-history -c T7837.hs -O -ddump-rule-firings >T7837.comp.stderr 2>&1 =====> T7837(profasm) 1395 of 4068 [0, 0, 0] cd ./indexed-types/should_compile && '/Users/jrp/Projects/haskell/ghc/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-db -rtsopts -fno-ghci-history -c T7837.hs -O -prof -static -auto-all -O -ddump-rule- firings >T7837.comp.stderr 2>&1 Actual stderr output differs from expected: --- ./indexed-types/should_compile/T7837.stderr 2014-08-03 11:36:53.000000000 +0100 +++ ./indexed-types/should_compile/T7837.comp.stderr 2014-08-04 23:16:34.000000000 +0100 @@ -1,3 +1,4 @@ Rule fired: Class op abs Rule fired: Class op signum Rule fired: normalize/Double +Rule fired: Class op / *** unexpected failure for T7837(profasm) Unexpected results from: TEST="T7837" OVERALL SUMMARY for test run started at Mon Aug 4 23:16:32 2014 BST 0:00:02 spent to go through 4068 total tests, which gave rise to 19536 test cases, of which 19534 were skipped 0 had missing libraries 1 expected passes 0 expected failures 0 caused framework failures 0 unexpected passes 1 unexpected failures Unexpected failures: indexed-types/should_compile T7837 [stderr mismatch] (profasm) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9406> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8