Opened 6 months ago

Closed 6 months ago

#16410 closed bug (duplicate)

Order of declarations matters

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #12088 Differential Rev(s):
Wiki Page:

Description

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.

Change History (4)

comment:1 Changed 6 months ago by int-index

My gut instinct is that this is another instance of #12088.

comment:2 Changed 6 months ago by Iceland_jack

I get similar behavior for

{-# Language DataKinds              #-}
{-# Language GADTs                  #-}
{-# Language PolyKinds              #-}
{-# Language TypeFamilyDependencies #-}
{-# Language TypeOperators          #-}
{-# Language UndecidableInstances   #-}

import Data.Kind
-- import Data.Type.Equality

class Category (tag::Type) where
 type Strip (tag::Type)

class Category tag => Stripped tag where
 type Hom tag = (res::Strip tag -> Strip tag -> Type) | res -> tag

data REFL (k :: Type) :: Type
data a :~: b where
 Refl :: a :~: a

instance Category (REFL k) where
 type Strip (REFL k) = k
instance Stripped (REFL k) where
 type Hom (REFL k) = (:~:)

This works.

Moving (:~:) above REFL fails

    Type family equation violates injectivity annotation.
    Type variable ‘k’ cannot be inferred from the right-hand side.
    In the type family equation:
      Hom (REFL k) = (:~:) -- Defined at 1154_bug.hs:24:7
   |
24 |  type Hom (REFL k) = (:~:)
   |       ^^^
Failed, no modules loaded.

Similarly removing the (:~:) declaration and importing it from Data.Type.Equality yields the same failure.

Last edited 6 months ago by Iceland_jack (previous) (diff)

comment:3 Changed 6 months ago by simonpj

My gut instinct is that this is another instance of #12088.

Mine too - but I have not investigated properly

comment:4 Changed 6 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

Indeed, this is a duplicate of #12088. Note that the same workaround applies here: you can use a Template Haskell splice to force the dependency analysis to come to its senses. That is, the following typechecks (note the addition of the $(pure []) bit):

{-# Language DataKinds    #-}
{-# Language GADTs        #-}
{-# Language InstanceSigs #-}
{-# Language PolyKinds    #-}
{-# Language TypeFamilies #-}
{-# LANGUAGE TemplateHaskell #-}

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 = ()

$(pure [])

instance Stripped Tag where
 type Hom Tag = Unit1
Note: See TracTickets for help on using tickets.