#14515 closed bug (fixed)

"Same" higher-rank kind synonyms behave differently

Reported by: Iceland_jack 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: GHC rejects valid program Test Case: polykinds/T14515
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

As you know type-level foralls don't float, so we may want to write HRefl's kind

-- Different from
--   HREFL :: forall k1 k2. k1 -> k2 -> Type
-- 
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
  HREFL :: HREFL a a

Let us capture forall k2. k2 -> .. with a kind synonym

type HRank2 ty = forall k2. k2 -> ty

data HREFL :: forall k. k -> HRank2 Type where
  HREFL :: HREFL a a

Works fine. Phew. Let's do the same for forall k1. k1 -> ..

type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty

data HREFL :: HRank1 (HRank2 Type) where
  HREFL :: HREFL a a 

Works fine. Phew.

“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!

data HREFL :: HRank1 (HRank1 Type) -- FAILS
data HREFL :: HRank1 (HRank2 Type) -- OK
data HREFL :: HRank2 (HRank1 Type) -- OK 
data HREFL :: HRank2 (HRank2 Type) -- FAILS
$ ghci -ignore-dot-ghci /tmp/Weird.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/Weird.hs, interpreted )

/tmp/Weird.hs:8:1: error:
    • These kind and type variables: (b :: k2) k2 (d :: k2)
      are out of dependency order. Perhaps try this ordering:
        k2 (b :: k2) (d :: k2)
    • In the data type declaration for ‘HREFL’
  |
8 | data HREFL :: HRank2 (HRank2 Type) 
  | ^^^^^^^^^^
Failed, 0 modules loaded.
Prelude> 

Same happens defining HRank2 in terms of HRank1

type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = HRank1 ty

Change History (3)

comment:1 Changed 13 months ago by RyanGlScott

Component: CompilerCompiler (Type checker)
Keywords: TypeInType added
Type of failure: None/UnknownGHC rejects valid program

For the sake of convenience, here's all of the various combinations in one file:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty

data HREFL11 :: HRank1 (HRank1 Type) where
  HREFL11 :: HREFL11 a a

data HREFL12 :: HRank1 (HRank2 Type) where
  HREFL12 :: HREFL12 a a

data HREFL21 :: HRank2 (HRank1 Type) where
  HREFL21 :: HREFL21 a a

data HREFL22 :: HRank2 (HRank2 Type) where
  HREFL22 :: HREFL22 a a

comment:2 Changed 13 months ago by Iceland_jack

The constructor isn't necessary to trigger it

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty

data HREFL11 :: HRank1 (HRank1 Type) -- FAILS
data HREFL12 :: HRank1 (HRank2 Type)
data HREFL21 :: HRank2 (HRank1 Type)
data HREFL22 :: HRank2 (HRank2 Type) -- FAILS

comment:3 Changed 12 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T14515

Great examples! Fixed by

commit 68149452a793aedd8d468b689dc93fb2ba5ec436
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Fri Dec 15 09:29:12 2017 +0000

    Fix tcDataKindSig
    
    This patch fixes an outright bug in tcDataKindSig, shown up in Trac
    of a data type declaration.  See Note [TyConBinders for the result kind
    signature of a data type]
    
    I also took the opportunity to elminate the DataKindCheck argument
    and data type from tcDataKindSig, instead moving the check to the
    call site, which is easier to understand.


>---------------------------------------------------------------

68149452a793aedd8d468b689dc93fb2ba5ec436
 compiler/typecheck/TcHsType.hs             | 126 +++++++++++++++++------------
 compiler/typecheck/TcInstDcls.hs           |  20 ++---
 compiler/typecheck/TcTyClsDecls.hs         |  22 +++--
 compiler/types/Type.hs                     |  16 +---
 testsuite/tests/ghci/scripts/T13407.stdout |   2 +-
 testsuite/tests/polykinds/T14515.hs        |  13 +++
 testsuite/tests/polykinds/all.T            |   1 +
 7 files changed, 116 insertions(+), 84 deletions(-)

Note: See TracTickets for help on using tickets.