Opened 11 months ago

Last modified 2 weeks 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: #12088, #12643, #15561, #15987 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 (8)

comment:1 Changed 11 months ago by heptahedron

Keywords: TypeInType added

comment:2 Changed 11 months ago by goldfire

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

comment:3 Changed 11 months ago by simonpj

May, possibly, relate to #12088 or #14451

comment:4 Changed 10 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 10 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 10 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!

comment:7 Changed 2 weeks ago by RyanGlScott

This is almost surely a duplicate of #12088 (see also #12643, #15561, and #15987, which are other surely-duplicates of #12088).

Here are two tricks to making these sorts of programs compile:

  1. TemplateHaskell. Using an empty Template Haskell splice can often force GHC's SCC analysis to come to its senses and do the right thing. As an example, the following variations of danilo2's program in comment:4 compiles:
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

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 KeyKind (Map k v) = k
type instance ValKind (Map k v) = v

$(pure [])

type instance Get k ('Map ('(k,v) ': _)) = v
  1. Closed type families. As I discovered recently in #15987, open and closed type families behave differently in SCC analysis, so it turns out that turning ValKind into a closed type family makes danilo2's program compile as well:
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

module Type.Data.Map where

import Prelude
import Data.Kind


type family KeyKind (obj :: Type) :: Type
type family ValKind (obj :: Type) :: Type where
  ValKind (Map k v) = v

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
Last edited 2 weeks ago by RyanGlScott (previous) (diff)

comment:8 Changed 2 weeks ago by RyanGlScott

Note: See TracTickets for help on using tickets.