[GHC] #9200: Milner-Mycroft failure at the kind level

12 Jun 2014

      #9200: Milner-Mycroft failure at the kind level
-------------------------------------+-------------------------------------
       Reporter:  ekmett             |             Owner:
           Type:  bug                |            Status:  new
       Priority:  normal             |         Milestone:
      Component:  Compiler (Type     |           Version:  7.8.2
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 This is a reduction of a problem that occurs in real code.

 {{{
 {-# LANGUAGE PolyKinds #-}
 class D a => C (f :: k) a
 class C () a => D a
 }}}

 Typechecking complains:

 {{{
     The first argument of ‘C’ should have kind ‘k’,
       but ‘()’ has kind ‘*’
     In the class declaration for ‘D’
 }}}

 This program should be accepted, but we're not generalizing enough.

 A slightly less reduced version of the problem arises in practice in:

 {{{
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PolyKinds #-}

 import Control.Category

 class (Category c, Category d, Category e) => Profunctor
   (p :: x -> y -> z)
   (c :: x -> x -> *)
   (d :: y -> y -> *)
   (e :: z -> z -> *)
   | p -> c d e

 -- lens-style isomorphism families in an arbitrary category
 type Iso (c :: i -> i -> *) (s :: i) (a :: i) = forall (p :: i -> i -> *).
   Profunctor p c c (->) => p a a -> p s s

 class Category e => Cartesian (e :: z -> z -> *) where
   type P e :: z -> z -> z
   associate :: Iso e (P e (P e a b) c) (P e a (P e b c))
 }}}

 This typechecks, but if I replace the line

 {{{
 class (Category c, Category d, Category e) => Profunctor
 }}}

 with

 {{{
 class (Category c, Category d, Cartesian e) => Profunctor
 }}}

 to say that you can only enrich a category over a monoidal category (using
 `Cartesian` in the approximation here), then it fails because a more
 baroque version of the same kind of cycle as the minimal example above as
 Profunctor references Cartesian which references an Iso which mentions a
 Profunctor.

 I'm supplying explicit kind variables in the signature of the class, so we
 should be able to use those like we do with function signatures a universe
 down. =/

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler