Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds)
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 (closed). 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 (closed)?
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |