September 2018 - ghc-tickets

[GHC] #12160: MonadFail instance for (Either String)?
by GHC 25 Oct '18

25 Oct '18

#12160: MonadFail instance for (Either String)? -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: libraries | Version: 8.0.1 (other) | 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 think one of the cool things about breaking out `MonadFail` would be the opportunity to introduce an instance for `Either String`, which isn’t possible to do with plain `Monad` without overlapping instances. The instance itself would be completely trivial: {{{#!hs instance MonadFail (Either String) where fail = Left }}} The only possible reason to ''not'' do this, as far as I can tell, would be because it requires `FlexibleInstances`. This already seems to be used for a few instances in `base`, and it seems like it would be extremely useful, so I would really appreciate if such an instance was defined. I’d be happy to submit a patch to add it, but I wasn’t sure if this would be an uncontroversial change or not. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12160> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15

[GHC] #14332: Deriving clauses can have forall types
by GHC 25 Oct '18

25 Oct '18

#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: deriving | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I made a horrifying discovery today: GHC accepts this code! {{{#!hs {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -ddump-deriv #-} module Bug1 where class C a b data D a = D deriving ((forall a. C a)) }}} {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug1 ( Bug.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance Bug1.C a1 (Bug1.D a2) where Derived type family instances: Ok, 1 module loaded. }}} It gets even worse with this example: {{{#!hs {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} {-# OPTIONS_GHC -ddump-deriv -fprint-explicit-kinds #-} module Bug1 where import Data.Kind import GHC.Generics data Proxy (a :: k) = Proxy deriving ((forall k. (Generic1 :: (k -> Type) -> Constraint))) }}} {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug1 ( Bug.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance GHC.Generics.Generic1 k (Bug1.Proxy k) where GHC.Generics.from1 x_a3ip = GHC.Generics.M1 (case x_a3ip of { Bug1.Proxy -> GHC.Generics.M1 GHC.Generics.U1 }) GHC.Generics.to1 (GHC.Generics.M1 x_a3iq) = case x_a3iq of { (GHC.Generics.M1 GHC.Generics.U1) -> Bug1.Proxy } Derived type family instances: type GHC.Generics.Rep1 k_a2mY (Bug1.Proxy k_a2mY) = GHC.Generics.D1 k_a2mY ('GHC.Generics.MetaData "Proxy" "Bug1" "main" 'GHC.Types.False) (GHC.Generics.C1 k_a2mY ('GHC.Generics.MetaCons "Proxy" 'GHC.Generics.PrefixI 'GHC.Types.False) (GHC.Generics.U1 k_a2mY)) Ok, 1 module loaded. }}} In this example, the `forall`'d `k` from the `deriving` clause is discarded and then unified with the `k` from `data Proxy (a :: k)`. All of this is incredibly unsettling. We really shouldn't be allowing `forall` types in `deriving` clauses in the first place. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14332> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 18

[GHC] #15497: Coercion Quantification
by GHC 25 Oct '18

25 Oct '18

#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 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: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2 -------------------------------------+------------------------------------- As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2] We would like to have coercion quantifications back in Haskell Core language. This means in Core we can define types like {{{#!hs \/ (a: k1) . \/ (co : k1 ~ k2) -- an explicit quantification for the coercion -> (a |> co) -- use the name for an explicit cast -> ... }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #15589: Always promoting metavariables during type inference may be wrong
by GHC 25 Oct '18

25 Oct '18

#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.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: -------------------------------------+------------------------------------- Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes. Consider {{{#!hs {-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies, AllowAmbiguousTypes #-} import Data.Proxy import Data.Type.Equality import Data.Type.Bool import Data.Kind data SameKind :: forall k. k -> k -> Type type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where IfK (_ :: Proxy True) f _ = f IfK (_ :: Proxy False) _ g = g y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> () y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d x = undefined in () }}} This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it. * We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n`, where `If :: forall k. Bool -> k -> k -> k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator. * In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2. * If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem. * Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`. * Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late. Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed. An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=co… my thesis] -- section 6.5 to be specific.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15589> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #14859: Allow explicit impredicativity
by GHC 25 Oct '18

25 Oct '18

#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- In [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html this email] I suggested allowing a simple form of impredicativity. With a suitable extension flag (`-XExplicitImpredicativeTypes` perhaps), you woudl be allowed: * To write a polytype in a visible type argument; eg. `f @(forall a. a->a)` * To write a polytype as an argument of a type in a signature e.g. `f :: [forall a. a->a] -> Int` ''But that’s all''. A unification variable still cannot be unified with a polytype. The only way you can call a polymorphic function at a polytype is to use Visible Type Application (VTA). So using impredicative types might be tiresome. E.g. {{{ type SID = forall a. a->a xs :: [forall a. a->a] xs = (:) @SID id ( (:) @SID id ([] @ SID)) }}} In short, if you call a function at a polytype, you must use VTA. Simple, easy, predictable; and doubtless annoying. But at least it's possible. The main motivation is that we are naughtily doing this anyway in the implementation of `GeneralisedNewtypeDeriving` -- see Trac #14070 comment:23 ff. If we are doing it under the hood, we could just made it available to programmers. This is much less ambitious, and much easier to implement, than the proposed [https://www.microsoft.com/en-us/research/publication/guarded- impredicative-polymorphism/ Guarded impredicative polymorphism] (PLDI'18). This ticket just records the idea, to see what other use-cases people might want to add. Then someone would have to write a GHC proposal. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14859> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #15648: Core Lint error with source-level unboxed equality
by GHC 25 Oct '18

25 Oct '18

#15648: Core Lint error with source-level unboxed equality -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: #15209 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I thought that we had killed `(~#)` from the source language in #15209. I could not have been more wrong. Source-level `(~#)` is alive and well, and it can cause Core Lint errors. Be afraid. Be very, very afraid. The trick is to grab `(~#)` using Template Haskell: {{{#!hs module Foo where import Language.Haskell.TH.Lib import Language.Haskell.TH.Syntax ueqT :: Q Type ueqT = conT $ mkNameG_tc "ghc-prim" "GHC.Prim" "~#" }}} Once this is done, you can plop unboxed equality wherever you want into the source language. Here is a particularly mischievous example: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind (Type) import Data.Type.Equality (type (~~)) import Foo (ueqT) data LegitEquality :: Type -> Type -> Type where Legit :: LegitEquality a a data JankyEquality :: Type -> Type -> Type where Jank :: $ueqT a b -> JankyEquality a b unJank :: JankyEquality a b -> $ueqT a b unJank (Jank x) = x legitToJank :: LegitEquality a b -> JankyEquality a b legitToJank Legit = Jank mkLegit :: a ~~ b => LegitEquality a b mkLegit = Legit ueqSym :: forall (a :: Type) (b :: Type). $ueqT a b -> $ueqT b a ueqSym = unJank $ legitToJank $ mkLegit @b @a }}} If you compile this with optimizations, then GHC's inner demons are unleashed, which brings utter chaos when `-dcore-lint` is enabled: {{{ $ /opt/ghc/8.6.1/bin/ghc -O2 -fforce-recomp Bug.hs -dcore-lint [1 of 2] Compiling Foo ( Foo.hs, Foo.o ) [2 of 2] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Simplifier *** <no location info>: warning: [in body of lambda with binder co_a5RY :: a_a5RV ~# b_a5RW] x_a5OX :: b_a5RW ~# a_a5RV [LclId] is out of scope *** Offending Program *** <elided> ueqSym :: forall a b. (a ~# b) => b ~# a [LclIdX, Arity=1, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}] ueqSym = \ (@ a_a5RV) (@ b_a5RW) (co_a5RY :: a_a5RV ~# b_a5RW) -> x_a5OX }}} ----- Obviously, this ticket is a little tongue-in-cheek, since I'm probably inviting disaster upon myself by deliberately digging around in `ghc-prim` for `(~#)`. But this does raise the question: should we allow users to do this? I used to think that there was no harm in leaving `(~#)` lying at the bottom of the catacombs that is `ghc-prim`, but this example shows that perhaps `(~#)` should be locked away for good. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15648> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 17

[GHC] #15300: Unboxed Sums Crash
by GHC 25 Oct '18

25 Oct '18

#15300: Unboxed Sums Crash -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: UnboxedSums | 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've made it a little further in my experiments with unboxed tuples in the `packed` library. However, I've run into another issue that I strongly suspect is the result of bad behavior of unboxed tuples. To replicate this issue (with GHC 8.4.3), do the following: {{{ git clone https://github.com/andrewthad/packed cd packed cabal new-build }}} We use `cabal new-build` for its side effect of creating a `.ghc.environment.xyz` file. Now, create a minimal example in the directory called `eol.hs` with the following contents: {{{ import Packed.Bytes.Parser (Parser) import Data.Word import Packed.Bytes (Bytes) import GHC.Exts (RealWorld) import Packed.Bytes.Stream.IO (ByteStream) import qualified Packed.Bytes as B import qualified Data.Char import qualified Packed.Bytes.Parser as P import qualified Packed.Bytes.Stream.IO as Stream main :: IO () main = do r <- runExampleParser ( do P.takeBytesUntilEndOfLineConsume P.takeBytesUntilEndOfLineConsume P.takeBytesUntilEndOfLineConsume ) (foldMap Stream.singleton (map charToWord8 "the\nemporium\rhas\narrived")) print r runExampleParser :: Parser e () a -> ByteStream RealWorld -> IO (Maybe a, Maybe String) runExampleParser parser stream = do P.Result mleftovers r _ <- P.parseStreamIO stream () parser mextra <- case mleftovers of Nothing -> return Nothing Just (P.Leftovers chunk remainingStream) -> do bs <- Stream.unpack remainingStream return (Just (map word8ToChar (B.unpack chunk ++ bs))) return (either (const Nothing) Just r,mextra) word8ToChar :: Word8 -> Char word8ToChar = Data.Char.chr . fromIntegral charToWord8 :: Char -> Word8 charToWord8 = fromIntegral . Data.Char.ord s2b :: String -> Bytes s2b = B.pack . map charToWord8 c2w :: Char -> Word8 c2w = charToWord8 }}} Finally, build this with `ghc -O2 eol.hs`, and then run the executable this produces to get the following: {{{ (Nothing,Just "\rhas\narrived") eol: internal error: stg_ap_n_ret (GHC version 8.4.3 for x86_64_unknown_linux) Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug Aborted (core dumped) }}} Things worth noting: 1. I think the program fails in the final GC that runs right before the program terminates. We can see that it produces a correct result of `(Nothing,Just "\rhas\narrived")`, but something on the heap has definitely been corrupted. 2. This only happens with `-O2` turned on. 3. This only happens when the parser does not successfully parse its input. Here's some more context around this. I've been working on a parser that uses unboxed sums instead of continuations. After #15038 was fixed, everything had been going well. Then, I took the parser type and added two things to it: (1) context and (2) typed errors. Context is basically like throwing `StateT` on top and errors are like throwing `ExceptT` on top. After this, everything in my test suite kept working except for a single test, which now consistently crashes my test suite. So, I originally had this: {{{ type Bytes# = (# ByteArray#, Int#, Int# #) type Maybe# (a :: TYPE r) = (# (# #) | a #) type Leftovers# s = (# Bytes# , ByteStream s #) type Result# s (r :: RuntimeRep) (a :: TYPE r) = (# Maybe# (Leftovers# s), Maybe# a #) newtype ParserLevity (r :: RuntimeRep) (a :: TYPE r) = ParserLevity { getParserLevity :: forall s. Maybe# (Leftovers# s) -> State# s -> (# State# s, Result# s r a #) } }}} But I changed it to this: {{{ type Bytes# = (# ByteArray#, Int#, Int# #) type Maybe# (a :: TYPE r) = (# (# #) | a #) type Either# a (b :: TYPE r) = (# a | b #) type Leftovers# s = (# Bytes# , ByteStream s #) type Result# e c s (r :: RuntimeRep) (a :: TYPE r) = (# Maybe# (Leftovers# s), Either# (Maybe e) a, c #) newtype ParserLevity e c (r :: RuntimeRep) (a :: TYPE r) = ParserLevity { getParserLevity :: forall s. c -> Maybe# (Leftovers# s) -> State# s -> (# State# s, Result# e c s r a #) } }}} Specifically, the function causing trouble is (as currently defined): {{{ {-# NOINLINE takeBytesUntilEndOfLineConsumeUnboxed #-} takeBytesUntilEndOfLineConsumeUnboxed :: ParserLevity e c BytesRep Bytes# takeBytesUntilEndOfLineConsumeUnboxed = ParserLevity (go (# (# #) | #)) where go :: Maybe# Bytes# -> c -> Maybe# (Leftovers# s) -> State# s -> (# State# s, Result# e c s BytesRep Bytes# #) go !_ c (# (# #) | #) s0 = (# s0, (# (# (# #) | #), (# Nothing | #), c #) #) go !mbytes c (# | (# bytes0@(# arr0, off0, len0 #), !stream0@(ByteStream streamFunc) #) #) s0 = case BAW.findAnyByte2 (I# off0) (I# len0) 10 13 (ByteArray arr0) of Nothing -> case streamFunc s0 of (# s1, r #) -> go (# | appendMaybeBytes mbytes bytes0 #) c r s1 Just (I# ix, W8# theByte) -> case theByte of 10## -> (# s0, (# (# | (# unsafeDrop# ((ix -# off0) +# 1# ) bytes0, stream0 #) #), (# | appendMaybeBytes mbytes (# arr0, off0, ix -# off0 #) #), c #) #) -- second case means it was 13 _ -> case ix <# (off0 +# len0 -# 1#) of 1# -> case indexWord8Array# arr0 (ix +# 1# ) of 10## -> (# s0, (# (# | (# unsafeDrop# ((ix -# off0) +# 2# ) bytes0, stream0 #) #), (# | appendMaybeBytes mbytes (# arr0, off0, ix -# off0 #) #), c #) #) _ -> (# s0, (# (# | (# unsafeDrop# (ix -# off0) bytes0, stream0 #) #), (# Nothing | #), c #) #) _ -> case nextNonEmpty stream0 s0 of (# s1, m #) -> case m of (# (# #) | #) -> (# s1, (# (# | (# unboxBytes (B.singleton 13), Stream.empty #) #), (# Nothing | #), c #) #) (# | (# bytes1@(# arr1, _, _ #), stream1 #) #) -> case indexWord8Array# arr1 0# of 10## -> (# s1, (# (# | (# unsafeDrop# 1# bytes1, stream1 #) #), (# | appendMaybeBytes mbytes (# arr0, off0, ix -# off0 #) #), c #) #) _ -> (# s1, (# (# | (# unboxBytes (B.cons 13 (boxBytes bytes1)), stream1 #) #), (# Nothing | #), c #) #) }}} That's all I've got for now. If no one's able to make headway, I'll probably come back to this and try to make a more minimal example at some point. I won't have time to do this soon though. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15300> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 25

[GHC] #14398: Fail to install haskell platform on Windows
by GHC 25 Oct '18

25 Oct '18

#14398: Fail to install haskell platform on Windows -------------------------------------+------------------------------------- Reporter: KAAAsS | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 8.2.1 Keywords: | Operating System: Windows Architecture: x86_64 | Type of failure: Installing GHC (amd64) | failed Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I can't run WinGHCi after my installation. When I use command "ghci" in cmd, it returns: {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help ghc.exe: internal error: mkPath failed converting char* to wchar_t* (GHC version 8.2.1 for x86_64_unknown_mingw32) Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug This application has requested the Runtime to terminate it in an unusual way. Please contact the application's support team for more information. }}} I had tried to reinstall or download the Core(64-bit) version, but nothing changed. I think there's nothing wrong with my install precedure. Sorry for my poor English! BTW, my windows is under Chinese code system. I don't know whether this matters or not. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14398> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #15694: GHC panic from pattern synonym, "Type-correct unfilled coercion hole"
by GHC 24 Oct '18

24 Oct '18

#15694: GHC panic from pattern synonym, "Type-correct unfilled coercion hole" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language RankNTypes, PatternSynonyms, TypeOperators, DataKinds, PolyKinds, KindSignatures, GADTs #-} import Data.Kind import Data.Type.Equality data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as) data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where AO :: a -> ApplyT(Type) a E AS :: ApplyT(ks) (f a) ctx -> ApplyT(k -> ks) f (a:&:ctx) pattern ASSO :: () => forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks) (ks1 :: Type) k1 (a2 :: k1) (ctx1 :: Ctx ks1) a3. (kind ~ (k -> ks), a ~~ f, b ~~ (a1 :&: ctx), ks ~ (k1 -> ks1), ctx ~~ (a2 :&: E), ks1 ~ Type, f a1 a2 ~~ a3) => a3 -> ApplyT kind a b pattern ASSO a = AS (AS (AO a)) }}} {{{ baldur@KindStar:~/hs$ ghci -ignore-dot-ghci 465.hs GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 465.hs, interpreted ) WARNING: file compiler/types/TyCoRep.hs, line 2378 in_scope InScope {kind_a1Cw a_a1Cx b_a1Cy ks_a1Cz k_a1CA f_a1CB a1_a1CC ctx_a1CD ks1_a1CE k1_a1CF a2_a1CG ctx1_a1CH a3_a1CI k0_a1F8} tenv [a1Cw :-> kind_a1Cw[sk:0], a1Cx :-> a_a1Cx[sk:0], a1Cy :-> b_a1Cy[sk:0], a1Cz :-> ks_a1Cz[sk:0], a1CA :-> k_a1CA[sk:0], a1CB :-> f_a1CB[sk:0], a1CC :-> a1_a1CC[sk:0], a1CD :-> ctx_a1CD[sk:0], a1CE :-> ks1_a1CE[sk:0], a1CF :-> k1_a1CF[sk:0], a1CG :-> a2_a1CG[sk:0], a1CH :-> ctx1_a1CH[sk:0], a1CI :-> a3_a1CI[sk:0]] cenv [] tys [kind_a1Cw[sk:1] ~ (k_a1CA[sk:2] -> ks_a1Cz[sk:2]), a_a1Cx[sk:1] ~~ f_a1CB[sk:2], b_a1Cy[sk:1] ~~ (a1_a1CC[sk:2] ':&: ctx_a1CD[sk:2]), ks_a1Cz[sk:2] ~ (k1_a1CF[sk:2] -> ks1_a1CE[sk:2]), ctx_a1CD[sk:2] ~~ (a2_a1CG[sk:2] ':&: 'E), ks1_a1CE[sk:2] ~ *, (f_a1CB[sk:2] a1_a1CC[sk:2] |> {co_a1Fc}) a2_a1CG[sk:2] ~~ a3_a1CI[sk:2]] cos [] needInScope [a1F8 :-> k0_a1F8[sk:2], a1Fc :-> co_a1Fc] WARNING: file compiler/types/TyCoRep.hs, line 2378 in_scope InScope {kind_a1Cw a_a1Cx b_a1Cy k0_a1HA ks_a1HB k_a1HC f_a1HD a1_a1HE ctx_a1HF ks1_a1HG k1_a1HH a2_a1HI ctx1_a1HJ a3_a1HK} tenv [a1Cz :-> ks_a1HB[tau:4], a1CA :-> k_a1HC[tau:4], a1CB :-> f_a1HD[tau:4], a1CC :-> a1_a1HE[tau:4], a1CD :-> ctx_a1HF[tau:4], a1CE :-> ks1_a1HG[tau:4], a1CF :-> k1_a1HH[tau:4], a1CG :-> a2_a1HI[tau:4], a1CH :-> ctx1_a1HJ[tau:4], a1CI :-> a3_a1HK[tau:4], a1F8 :-> k0_a1HA[tau:4]] cenv [] tys [kind_a1Cw[sk:0] ~ (k_a1CA[sk:0] -> ks_a1Cz[sk:0]), a_a1Cx[sk:0] ~~ f_a1CB[sk:0], b_a1Cy[sk:0] ~~ (a1_a1CC[sk:0] ':&: ctx_a1CD[sk:0]), ks_a1Cz[sk:0] ~ (k1_a1CF[sk:0] -> ks1_a1CE[sk:0]), ctx_a1CD[sk:0] ~~ (a2_a1CG[sk:0] ':&: 'E), ks1_a1CE[sk:0] ~ *, (f_a1CB[sk:0] a1_a1CC[sk:0] |> {co_a1Fc}) a2_a1CG[sk:0] ~~ a3_a1CI[sk:0]] cos [] needInScope [a1Cw :-> kind_a1Cw[sk:0], a1Cx :-> a_a1Cx[sk:0], a1Cy :-> b_a1Cy[sk:0], a1Fc :-> co_a1Fc] ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20180828 for x86_64-unknown-linux): ASSERT failed! Type-correct unfilled coercion hole {co_a1Fc} Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1716:99 in ghc:TcHsSyn Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug > }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15694> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #12677: Type equality in constraint not used?
by GHC 24 Oct '18

24 Oct '18

#12677: Type equality in constraint not used? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | 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: -------------------------------------+------------------------------------- {{{#!hs data TyRep :: forall k. k -> Type where TyInt :: TyRep Int TyBool :: TyRep Bool TyMaybe :: TyRep Maybe TyApp :: TyRep f -> TyRep x -> TyRep (f x) }}} This is allowed: {{{#!hs zero :: TypeRep (a :: Type) -> a zero = undefined }}} but this is not {{{#!hs zero :: Type ~ k => TyRep (a :: k) -> a zero = undefined zero :: TyRep (a :: k) -> Type ~ k => a zero = undefined }}} {{{ tuHu.hs:20:35: error: … • Expected a type, but ‘a’ has kind ‘k’ • In the type signature: zero :: Type ~ k => R (a :: k) -> a Compilation failed. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12677> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6