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:

  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?

Attachments (1)

Testcase.hs (7.0 KB) - added by Iceland_jack 14 months ago.

Download all attachments as: .zip

Change History (7)

Changed 14 months ago by Iceland_jack

Attachment: Testcase.hs added

comment:1 Changed 14 months ago by Iceland_jack

Also true for

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 Polynomial.hs and Category.hs adapted:

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 

comment:2 Changed 14 months ago 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

comment:3 Changed 14 months ago by thomie

Cc: goldfire added
Component: CompilerCompiler (Type checker)
Keywords: TypeInType added

comment:4 Changed 14 months ago 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.)
  1. 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 simonpj

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

Last edited 14 months ago by simonpj (previous) (diff)

comment:6 Changed 5 days ago by goldfire

Keywords: TypeInType removed

Upon review, I don't think this is all that related to TypeInType.

Note: See TracTickets for help on using tickets.