Milner-Mycroft failure at the kind level
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. =/
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | ekmett |
Operating system | |
Architecture |