Need proper SCC analysis of type declarations, taking account of CUSKs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-}
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
type Cat ob = ob -> ob -> Type
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply (CompSym2 f g) a = Comp f g a
data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c)
type a·b = Apply a b
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' -> Cod f (f·a) (f·a')
type family
Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where
Comp f g a = f · (Apply g a)
This compiles, but if I replace the final line by
Comp f g a = f · (g · a)
oddly enough I get an error message about the method varpa
! Seemingly unrelated apart from using (·)
:
$ ghci2 hs/093-bug.hs
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/093-bug.hs, interpreted )
hs/093-bug.hs:23:33: error:
• Expected kind ‘i ~> i’, but ‘f’ has kind ‘i ~> j’
• In the first argument of ‘(·)’, namely ‘f’
In the second argument of ‘Cod’, namely ‘(f · a)’
In the type signature:
varpa :: Dom f a a' -> Cod f (f · a) (f · a')
|
23 | varpa :: Dom f a a' -> Cod f (f·a) (f·a')
| ^
Failed, 0 modules loaded.
Prelude>
NOW — let's randomly remove both lines that mention CompSym2
and it mysteriously works, again!
Apply
and (·)
seem to be equal up to variable names, I can't spot why
>> :set -fprint-explicit-foralls
>> :set -fprint-explicit-kinds
>> :set -fprint-explicit-coercions
>>
>> :kind Apply
Apply :: forall {a} {b}. (a ~> b) -> a -> b
>> :kind (·)
(·) :: forall {a} {k}. (a ~> k) -> a -> k
but it works if I define (·)
as a type family rather than a synonym:
type family
(f::a ~> b) · (x::a) :: b where
f · x = Apply f x
so it's some difference between synonyms and TFs, but is it intentional? It's certainly odd how the error messages jumped the varpa
method when we actually modified Comp
.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |