April 2018 - ghc-tickets

[GHC] #14897: QuantifiedConstraints: Can't print type of quantified constraint
by GHC 02 Apr '18

02 Apr '18

#14897: QuantifiedConstraints: Can't print type of quantified constraint -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- {{{#!hs {-# Language QuantifiedConstraints, FlexibleInstances, UndecidableInstances, MonoLocalBinds #-} class (forall xx. Functor (f xx)) => Functor' f instance (forall xx. Functor (f xx)) => Functor' f fmap' :: Functor' f => (b -> b') -> (f a b -> f a b') fmap' = fmap }}} load in ghci and check the type of `fmap'` {{{ $ ... -ignore-dot-ghci Bug2.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Bug2.hs, interpreted ) Ok, one module loaded. *Main> :t fmap' <interactive>:1:1: error: No instance for (Functor (f xx)) arising from a use of ‘fmap'’ *Main> }}} Simpler example {{{ GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Prelude> :set -XRankNTypes -XQuantifiedConstraints Prelude> let a :: (forall xx. Monoid (f xx)) => f a; a = mempty Prelude> :t a <interactive>:1:1: error: No instance for (Monoid (f xx)) arising from a use of ‘a’ Prelude> }}} I expected the same output as `:t +v` {{{ Prelude> :t +v a a :: (forall xx. Monoid (f xx)) => f a }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14897> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[GHC] #14991: GHC HEAD regression involving TYPEs in type families
by GHC 02 Apr '18

02 Apr '18

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (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: -------------------------------------+------------------------------------- This program typechecks on GHC 8.2.2 and 8.4.1: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind type family Promote (k :: Type) :: Type type family PromoteX (a :: k) :: Promote k type family Demote (k :: Type) :: Type type family DemoteX (a :: k) :: Demote k ----- -- Type ----- type instance Demote Type = Type type instance Promote Type = Type type instance DemoteX (a :: Type) = Demote a type instance PromoteX (a :: Type) = Promote a ----- -- Arrows ----- data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type instance Demote (a ~> b) = DemoteX a -> DemoteX b type instance Promote (a -> b) = PromoteX a ~> PromoteX b }}} However, it fails to typecheck on GHC HEAD: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:34:34: error: • Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’ • In the first argument of ‘(~>)’, namely ‘PromoteX a’ In the type ‘PromoteX a ~> PromoteX b’ In the type instance declaration for ‘Promote’ | 34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b | ^^^^^^^^^^ Bug.hs:34:48: error: • Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’ • In the second argument of ‘(~>)’, namely ‘PromoteX b’ In the type ‘PromoteX a ~> PromoteX b’ In the type instance declaration for ‘Promote’ | 34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b | ^^^^^^^^^^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14991> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #14119: Refactor type patterns
by GHC 02 Apr '18

02 Apr '18

#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: 12564, 14038 | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways: * They must never mention a `forall`. * They must never mention a context. (The context in a class instance head is a different part of the instance construct.) * They must never mention a type family. Types that appear as arguments on the LHS of a RULE should also be type patterns. Type patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types. I thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation. We could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in comment:6:ticket:14038. It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like "wobbly types" than OutsideIn. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #14992: Allow existentials to UNPACK
by GHC 02 Apr '18

02 Apr '18

#14992: Allow existentials to UNPACK -------------------------------------+------------------------------------- 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 {{{ data T a where MkT :: b -> (b->a) -> T a data Wuggle where MkW :: {-# UNPACK #-} !T Int -> Wuggle }}} Here `MkT` has an existential, but there is really no reason that it can't unpack into the data constructor for `MkW`. But it is currently rejected. Fixing this would require quite a bit of new plumbing. E.g. the existential type variable of the worker and wrapper would differ, which is not true today. But morally it's the Right Thing. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14992> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #14884: Type holes cause assertion failure in ghc-stage2 compiler during type checking
by GHC 02 Apr '18

02 Apr '18

#14884: Type holes cause assertion failure in ghc-stage2 compiler during type checking -------------------------------------+------------------------------------- Reporter: sighingnow | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: (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: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- ghc-stage2 panic! due to assertion failure when compiling the following code with `ghc-stage2 Bug.hs` {{{#!hs module Bug where x :: IO () x = _ print "abc" }}} Callstack: {{{ λ inplace\bin\ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180225 for x86_64-unknown-mingw32): ASSERT failed! t_a4ec[tau:2] 2 1 Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler\utils\Outputable.hs:1150:37 in ghc:Outputable pprPanic, called at compiler\utils\Outputable.hs:1206:5 in ghc:Outputable assertPprPanic, called at compiler\\typecheck\\TcType.hs:1187:83 in ghc:TcType CallStack (from -prof): TcInteract.solve_loop (compiler\typecheck\TcInteract.hs:(247,9)-(254,44)) TcInteract.solveSimples (compiler\typecheck\TcInteract.hs:(241,5)-(243,21)) TcRnDriver.simplifyTop (compiler\typecheck\TcRnDriver.hs:408:25-39) TcRnDriver.tcRnSrcDecls (compiler\typecheck\TcRnDriver.hs:254:25-65) }}} The failed assertion is `checkTcLevelInvariant ctxt_tclvl tv_tclvl` in `isTouchableMetaTyVar`: {{{#!hs isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool isTouchableMetaTyVar ctxt_tclvl tv | isTyVar tv -- See Note [Coercion variables in free variable lists] = ASSERT2( tcIsTcTyVar tv, ppr tv ) case tcTyVarDetails tv of MetaTv { mtv_tclvl = tv_tclvl } -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl, ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl ) tv_tclvl `sameDepthAs` ctxt_tclvl _ -> False | otherwise = False }}} Notice that the ghc-stage1 compiler doesn't panic and report the type hole correctly. This seems a regression and I have checked that ghc-8.2.2 also works well. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14884> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #11186: Give strong preference to type variable names in scope when reporting hole contexts
by GHC 02 Apr '18

02 Apr '18

#11186: Give strong preference to type variable names in scope when reporting hole contexts -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: typed-holes | 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 using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like {{{#!hs foo :: forall bar . ... foo = ... _ ... }}} and yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11186> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 9

Re: [GHC] #5910: Holes with other constraints
by GHC 02 Apr '18

02 Apr '18

#5910: Holes with other constraints -------------------------------------+------------------------------------- Reporter: xnyhps | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.5 checker) | Resolution: | Keywords: TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: holes => TypedHoles -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5910#comment:29> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[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