[GHC] #12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds)
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple UndecidableSuperClasses | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #11480 #12025 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The Glorious Glasgow Haskell Compilation System, version 8.0.1. Code taken from [https://gist.github.com/ekmett/b26363fc0f38777a637d gist] with {{{#!hs fmap :: p a b -> q (f a) (f b) }}} replaced by {{{#!hs fmap :: Dom f a b -> Cod f (f a) (f b) }}} If you enable `DataKinds` and `TypeInType` `:kind` will happily tell you its kind: {{{ ghci> :kind 'Main.Nat 'Main.Nat :: forall j i (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j). (FunctorOf p q f, FunctorOf p q g) => (forall (a :: i). Ob p a => q (f a) (g a)) -> Main.Nat p q f g }}} but if you try `:type Nat` it spits out a long list of unsolved constraints {{{ ghci> :type Nat <interactive>:1:1: error: solveWanteds: too many iterations (limit = 1) Unsolved: WC {wc_simple = [W] $dFunctor_ag3Y :: Main.Functor f_ag3S (CDictCan) [W] $dFunctor_ag4d :: Main.Functor g_ag3T (CDictCan) [D] _ :: Main.Functor s_ag51 (CDictCan) [D] _ :: Main.Functor s_ag5a (CDictCan) [D] _ :: Main.Functor s_ag4W (CDictCan) [D] _ :: Main.Functor s_ag55 (CDictCan) [D] _ :: Category s_ag51 (CDictCan) [D] _ :: Category s_ag5a (CDictCan) [D] _ :: Category s_ag4W (CDictCan) [D] _ :: Category s_ag55 (CDictCan) [W] hole{ag4Y} :: Dom g_ag3T ~ Dom f_ag3S (CNonCanonical) [W] hole{ag53} :: Cod g_ag3T ~ Cod f_ag3S (CNonCanonical) [D] _ :: Dom (Dom f_ag3S) ~ Op (Dom f_ag3S) (CNonCanonical) [D] _ :: Cod (Dom f_ag3S) }}} This seems like #11480. This makes undecidable superclasses a harsh master and raises two questions that I'll bundle together: 1. Why can the `:kind` be inferred but not the `:type`? It works when given extra information: {{{ ghci> :type Nat @_ @_ @(->) @(->) Nat @_ @_ @(->) @(->) :: (Cod g ~ (->), Dom g ~ (->), Cod f ~ (->), Dom f ~ (->), Main.Functor g, Main.Functor f) => (forall a. Vacuous (->) a => f a -> g a) -> Main.Nat (->) (->) f g }}} {{{ ghci> :type Nat @_ @_ @_ @_ @[] @Maybe Nat @_ @_ @_ @_ @[] @Maybe :: (forall a. Vacuous (->) a => [a] -> Maybe a) -> Main.Nat (->) (->) [] Maybe }}} {{{ ghci> :type Nat @_ @_ @_ @_ @[] @Maybe listToMaybe Nat @_ @_ @_ @_ @[] @Maybe listToMaybe :: Main.Nat (->) (->) [] Maybe }}} 2. Why is `j` positioned before `i` (most likely because of `forall a. ...` but I tried tinkering without success? Is there any trick to ordering it as you'd expect `forall i j (p :: Cat i) (q :: Cat j)` or is it not possible per #12025? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11480 #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * Attachment "Testcase.hs" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11480 #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Also true for {{{#!hs data Product (p :: Cat i) (q :: Cat j) :: Cat (i, j) where Product :: p (Fst a) (Fst b) -> q (Snd a) (Snd b) -> Product p q a b }}} with code from [https://github.com/ekmett/hask/blob/master/src/Hask/Category/Polynomial.hs Polynomial.hs] and [https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs Category.hs] adapted: {{{#!hs type family Fst (p :: (i,j)) :: i where Fst '(a, _) = a type family Snd (q :: (i,j)) :: j where Snd '(_, b) = b type family NatDom (f :: Cat (i -> j)) :: Cat i where NatDom (Nat p _) = p type family NatCod (f :: Cat (i -> j)) :: Cat j where NatCod (Nat _ q) = q type Opd f = Op (Dom f) type Dom2 p = NatDom (Cod p) type Cod2 p = NatCod (Cod p) class (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: Cat i) (q :: Cat j) (a :: (i,j)) instance (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: Cat i) (q :: Cat j) (a :: (i,j)) instance (Category p, Category q) => Functor (Product p q) where type Dom (Product p q) = Op (Product (Opd p) (Opd q)) type Cod (Product p q) = Nat (Product (Dom2 p) (Dom2 q)) (->) instance (Category p, Category q, ProductOb p q a) => Functor (Product p q a) where type Dom (Product p q a) = Product (Dom2 p) (Dom2 q) type Cod (Product p q a) = (->) fmap = (.) instance (Category p, Category q) => Category (Product p q) where type Ob (Product p q) = ProductOb p q id = Product id id Product f f' . Product g g' = Product (f . g) (f' . g') target = undefined source = undefined }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11480 #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): `Product` doesn't make ghc spin, but oddly `j` appears before `i` even though `Cat i` appears before `Cat j`, etc. {{{ ghci> :t Product Product :: forall j i (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i, j)) (b :: (i, j)). p (Fst a) (Fst b) -> q (Snd a) (Snd b) -> Product p q a b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | UndecidableSuperClasses, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11480 #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * keywords: UndecidableSuperClasses => UndecidableSuperClasses, TypeInType * cc: goldfire (added) * component: Compiler => Compiler (Type checker) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | UndecidableSuperClasses, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11480 #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 1. `:kind` is much simpler than `:type`. `:kind` just reports the kind of the thing it sees. `:type`, on the other hand, instantiates, solves, and regeneralizes. It's the solver that's looping, so that's why only `:type` fails. (See #11376 for more info about why `:type` does this, and #11975 for a proposed refinement of `:type` that will allow `:kind`-like behavior.) 2. I think the algorithm that walks over the kind of a tycon and pulls out undeclared kind variables gets this backwards. I'm pretty sure that this has been reported elsewhere, but I can't find the ticket. In any case, I don't think anything deep is going on here. Let's not lose the big picture, though: the real problem in this ticket is that the solver loops, and that's what needs to be addressed. (I don't have further commentary on that point.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | UndecidableSuperClasses, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11480 #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: ekmett (added) Comment: The code in the Description is, I think, essentially the same as that in #11523. In comment:14 of that ticket I explain why I think there is a truly infinite tower of superclasses. If there is, GHC is likely to spin, and I don't know how to prevent that. Edward claims that there isn't an infinite tower, but I think he's wrong. But I believe he probably doesn't ''intend'' there to be one. So these tickets are stalled on resolving the question of what is really intended here Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11480 #12025 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: UndecidableSuperClasses, TypeInType => UndecidableSuperClasses Comment: Upon review, I don't think this is all that related to `TypeInType`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12131#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC