#9574: GHC Panic: No Skolem Info -------------------------------------+------------------------------------- Reporter: ian_mi | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Old description:

GHC 7.8.3 and from git both panic with

Couldn't match kind ‘o1’ with ‘(,) o o’ ‘o1’ is untouchable inside the constraints (Object (c :><: c) a) bound by a type expected by the context: Object (c :><: c) a => Tagged a (c (FMap (ProductF c) a) (FMap (Proj2 c c) a)) at Product.hs:35:9-15ghc: panic! (the 'impossible' happened) (GHC version 7.9.20140908 for x86_64-unknown-linux): No skolem info: o1_a6XS

I have not yet attempted to reduce the problem at all. The offending code is the use of fmap here:

{{{#!hs proj2 :: forall (c :: o -> o -> *). ProductCategory c => NatTr (c :><: c) c (ProductF c) (Proj2 c c) proj2 = NatTr t where NatTr t = fmap (CompF Proj2 IdentityF) e e :: NatTr (c :><: c) (c :><: c) (Comp ('KProxy :: KProxy o) (Diag c) (ProductF c)) (IdentityF (c :><: c)) e = counit }}}

fmap is defined as

{{{#!hs fmap :: forall f (a :: o1) (b :: o1). Functor f ('KProxy :: KProxy (o1 -> o2)) => f -> Domain f a b -> Codomain f (FMap f a :: o2) (FMap f b :: o2) fmap _ = proxy morphMap (Proxy :: Proxy f) }}}

while CompF is defined by

{{{#!hs data CompF f g (k :: KProxy (o3 -> o4, o1 -> o2)) where CompF :: (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o1 -> o2))) => f -> g -> CompF f g ('KProxy :: KProxy (o3 -> o4, o1 -> o2)) }}}

This makes some sense because there is a functional dependency between the functor and the kind proxy.

New description: GHC 7.8.3 and from git both panic with {{{ Couldn't match kind ‘o1’ with ‘(,) o o’ ‘o1’ is untouchable inside the constraints (Object (c :><: c) a) bound by a type expected by the context: Object (c :><: c) a => Tagged a (c (FMap (ProductF c) a) (FMap (Proj2 c c) a)) at Product.hs:35:9-15ghc: panic! (the 'impossible' happened) (GHC version 7.9.20140908 for x86_64-unknown-linux): No skolem info: o1_a6XS }}} I have not yet attempted to reduce the problem at all. The offending code is the use of fmap here: {{{#!hs proj2 :: forall (c :: o -> o -> *). ProductCategory c => NatTr (c :><: c) c (ProductF c) (Proj2 c c) proj2 = NatTr t where NatTr t = fmap (CompF Proj2 IdentityF) e e :: NatTr (c :><: c) (c :><: c) (Comp ('KProxy :: KProxy o) (Diag c) (ProductF c)) (IdentityF (c :><: c)) e = counit }}} fmap is defined as {{{#!hs fmap :: forall f (a :: o1) (b :: o1). Functor f ('KProxy :: KProxy (o1 -> o2)) => f -> Domain f a b -> Codomain f (FMap f a :: o2) (FMap f b :: o2) fmap _ = proxy morphMap (Proxy :: Proxy f) }}} while CompF is defined by {{{#!hs data CompF f g (k :: KProxy (o3 -> o4, o1 -> o2)) where CompF :: (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o1 -> o2))) => f -> g -> CompF f g ('KProxy :: KProxy (o3 -> o4, o1 -> o2)) }}} This makes some sense because there is a functional dependency between the functor and the kind proxy. -- Comment (by simonpj): Clearly a bug, but there's virtually no chance of fixing it without a way to reproduce it, alas. So if you felt able to do that, it'd be great. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9574#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9574: GHC Panic: No Skolem Info -------------------------------------+------------------------------------- Reporter: ian_mi | Owner: Type: bug | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by ian_mi): Sure. I've been trying to reduce it myself but it's been somewhat tricky. I will put together an unreduced example instead. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9574#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9574: GHC Panic: No Skolem Info -------------------------------------+------------------------------------- Reporter: ian_mi | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by ian_mi): * status: infoneeded => new Comment: Sorry for the delay, here is how this bug can be reproduced: 1. Clone the extended-categories package from https://github.com/ian-mi /extended-categories and checkout tag `0.2.0`. 2. Install the dependencies `tagged` and `constraints` into a sandbox if not already available. 3. Download the attached `Bug9574.hs` file. 3. Using GHC 7.8.3, load extended-categories into ghci using `cabal repl` and then load `Bug9574.hs`. Please let me know if you need any additional information. Thanks, Ian -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9574#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9574: GHC Panic: No Skolem Info -------------------------------------+------------------------------------- Reporter: ian_mi | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"171101beca39befde191baff5027c417bcc709ee/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="171101beca39befde191baff5027c417bcc709ee" Kind variables in RHS of an associated type instances should be bound on LHS This patche fixes Trac #9574. The previous Note [Renaming associated types] in RnTypes appears to me to be wrong; it confused class and instance declarations. I have: * Treated kind and type variables uniformly. Both must be bound on the LHS of an associated type instance. Eg instance C ('KProxy :: KProxy o) where type F 'KProxy = NatTr (Proxy :: o -> *) is illegal because 'o' is not bound on the LHS of the instance. * Moved the Note to RnSource and fixed it up This improves the error message from T7938. However it made the code in T6118 incorrect. We had: instance SingE (a :: Maybe k) where type Demote a = Maybe (Demote (Any :: k)) and that is now rejected, rightly I think. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9574#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9574: GHC Panic: No Skolem Info -------------------------------------+------------------------------------- Reporter: ian_mi | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T9574 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): -------------------------------------+------------------------------------- Comment (by Ryan Scott ): In [changeset:"0829821a6b886788a3ba6989e57e25a037bb6d05/ghc" 0829821a/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="0829821a6b886788a3ba6989e57e25a037bb6d05" Implicitly bind kind variables in type family instance RHSes when it's sensible Summary: Before, there was a discrepancy in how GHC renamed type synonyms as opposed to type family instances. That is, GHC would accept definitions like this one: ```lang=haskell type T = (Nothing :: Maybe a) ``` However, it would not accept a very similar type family instance: ```lang=haskell type family T :: Maybe a type instance T = (Nothing :: Maybe a) ``` The primary goal of this patch is to bring the renaming of type family instances up to par with that of type synonyms, causing the latter definition to be accepted, and fixing #14131. In particular, we now allow kind variables on the right-hand sides of type (and data) family instances to be //implicitly// bound by LHS type (or kind) patterns (as opposed to type variables, which must always be explicitly bound by LHS type patterns only). As a consequence, this allows programs reported in #7938 and #9574 to typecheck, whereas before they would have been rejected. Implementation-wise, there isn't much trickery involved in making this happen. We simply need to bind additional kind variables from the RHS of a type family in the right place (in particular, see `RnSource.rnFamInstEqn`, which has undergone a minor facelift). While doing this has the upside of fixing #14131, it also made it easier to trigger #13985, so I decided to fix that while I was in town. This was accomplished by a careful blast of `reportFloatingKvs` in `tcFamTyPats`. Test Plan: ./validate Reviewers: simonpj, goldfire, austin, bgamari Reviewed By: simonpj Subscribers: rwbarton, thomie GHC Trac Issues: #13985, #14131 Differential Revision: https://phabricator.haskell.org/D3872 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9574#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler