[GHC] #12131: Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds)

29 May 2016

      #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