Opened 14 months ago
Last modified 5 days ago
#12131 new bug
Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds)
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.0.1 |
Keywords: | UndecidableSuperClasses | Cc: | goldfire, ekmett |
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: |
Description
The Glorious Glasgow Haskell Compilation System, version 8.0.1.
Code taken from gist with
fmap :: p a b -> q (f a) (f b)
replaced by
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:
- 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
- Why is
j
positioned beforei
(most likely because offorall a. ...
but I tried tinkering without success? Is there any trick to ordering it as you'd expectforall i j (p :: Cat i) (q :: Cat j)
or is it not possible per #12025?
Attachments (1)
Change History (7)
Changed 14 months ago by
Attachment: | Testcase.hs added |
---|
comment:1 Changed 14 months ago by
comment:2 Changed 14 months ago by
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
comment:3 Changed 14 months ago by
Cc: | goldfire added |
---|---|
Component: | Compiler → Compiler (Type checker) |
Keywords: | TypeInType added |
comment:4 Changed 14 months ago by
: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.)
- 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.)
comment:5 Changed 14 months ago by
Cc: | ekmett added |
---|
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; I claim he's wrong; we can't both be right. So these tickets are stalled on resolving the question of what is really intended here.
Simon
comment:6 Changed 5 days ago by
Keywords: | TypeInType removed |
---|
Upon review, I don't think this is all that related to TypeInType
.
Also true for
with code from Polynomial.hs and Category.hs adapted: