Opened 5 months ago

Last modified 4 months ago

#14668 new bug

Ordering of declarations can cause typechecking to fail

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

Description

The following will successfully typecheck:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}

data CInst

data G (b :: ()) = G 

class C a where
  type family F a
  
class (C a) => C' a where
  type family F' a (b :: F a)

-- data CInst

instance C CInst where
  type F CInst = ()

instance C' CInst where
type F' CInst (b :: F CInst) = G b

But if the data CInst declaration is moved to where it is currently commented out, typechecking fails with this error:

Test.hs:23:18: error:
    • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
    • In the second argument of ‘F'’, namely ‘(b :: F CInst)’
      In the type instance declaration for ‘F'’
      In the instance declaration for ‘C' CInst’
   |
23 |   type F' CInst (b :: F CInst) = G b
   | 

However, the data declaration can be in the lower position if the kind annotation for its argument is instead written as data G (b :: F CInst) = G.

This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).

I was using GHC 8.2.2 when I discovered this, but user erisco on #haskell confirmed for 8.2.1 as well.

Change History (6)

comment:1 Changed 5 months ago by heptahedron

Keywords: TypeInType added

comment:2 Changed 5 months ago by goldfire

Thanks for the report! The TypeInType keyword makes sure it's in my queue.

comment:3 Changed 5 months ago by simonpj

May, possibly, relate to #12088 or #14451

comment:4 Changed 4 months ago by danilo2

Hi! Yet another example which seems related! If you move the data declaration to be the first line, it compiles fine:

{-# LANGUAGE TypeInType #-}

module Type.Data.Map where

import Prelude
import Data.Kind


type family KeyKind (obj :: Type) :: Type
type family ValKind (obj :: Type) :: Type

type family Get (key :: KeyKind a) (obj :: a) :: ValKind a

data Map (k :: Type) (v :: Type) = Map [(k,v)]

type instance Get k ('Map ('(k,v) ': _)) = v

type instance KeyKind (Map k v) = k
type instance ValKind (Map k v) = v

Otherwise it gives error:

Main.hs:16:19: error:
    • Occurs check: cannot construct the infinite kind:
        k0 ~ KeyKind (Map k0 v0)
      The type variables ‘v0’, ‘k0’ are ambiguous
    • In the first argument of ‘Get’, namely ‘k’
      In the type instance declaration for ‘Get’
   |         
16 | type instance Get k ('Map ('(k,v) ': _)) = v
   |                   ^
             
Main.hs:16:44: error:
    • Occurs check: cannot construct the infinite kind:
        v0 ~ ValKind (Map k0 v0)
      The type variables ‘k0’, ‘v0’ are ambiguous
    • In the type ‘v’
      In the type instance declaration for ‘Get’
   |         
16 | type instance Get k ('Map ('(k,v) ': _)) = v

comment:5 Changed 4 months ago by danilo2

What is even worse, this bug prevents us from refactoring the code to separate module, so I have to have the Get declaration in he same file, under all data definitions that are used to make instances of it.

comment:6 Changed 4 months ago by simonpj

What is even worse, this bug prevents us from refactoring the code to separate module

That's odd. The original report is about ordering declarations within a single module. Can you give a repro case for how refactoring your code into separate modules makes things fail? Thanks!

Note: See TracTickets for help on using tickets.