Order of declarations matters
This piece of code works.
{-# Language DataKinds #-}
{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language PolyKinds #-}
{-# Language TypeFamilies #-}
import Data.Kind
class Category (tag::Type) where
type Strip tag :: Type
class Category tag => Stripped tag where
type Hom tag::Strip tag -> Strip tag -> Type
instance Category () where
type Strip () = ()
instance Stripped () where
type Hom () = Unit1
data Unit1 :: () -> () -> Type where U1 :: Unit1 '() '()
data Tag
data Unit2 :: () -> () -> Type where U2 :: Unit2 '() '()
instance Category Tag where
type Strip Tag = ()
instance Stripped Tag where
type Hom Tag = Unit2
Note that Unit1
and Unit2
are declared identically, separated by data Tag
. The order is important.
If we change the last line to Hom Tag = Unit1
(same as Hom ()
) we get
$ ghc -ignore-dot-ghci 1152_bug.hs
GHCi, version 8.7.20190115: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 1152_bug.hs, interpreted )
1152_bug.hs:28:18: error:
• Expected kind ‘Strip Tag -> Strip Tag -> *’,
but ‘Unit1’ has kind ‘() -> () -> *’
• In the type ‘Unit1’
In the type instance declaration for ‘Hom’
In the instance declaration for ‘Stripped Tag’
|
28 | type Hom Tag = Unit1
| ^^^^^
Failed, no modules loaded.
Prelude>
even though Strip Tag
is defined to equal ()
. Here comes the weird part.
If I move Unit1
decl beneath data Tag
data Tag
data Unit1 :: () -> () -> Type where U1 :: Unit1 '() '()
data Unit2 :: () -> () -> Type where U2 :: Unit2 '() '()
then type Hom Tag = Unit1
and type Hom Tag = Unit2
both work well.
If I move Unit2
decl above data Tag
then both Hom Tag = Unit1
and Hom Tag = Unit2
fail!
data Unit1 :: () -> () -> Type where U1 :: Unit1 '() '()
data Unit2 :: () -> () -> Type where U2 :: Unit2 '() '()
data Tag
If I replace all occurrences of Tag
with Bool
it succeeds.
Trac metadata
Trac field | Value |
---|---|
Version | 8.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |