Opened 17 months ago

Closed 4 months ago

#11966 closed bug (fixed)

Surprising behavior with higher-rank quantification of kind variables

Reported by: ocharles Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.0.1-rc3
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: dependent/should_compile/T11966
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Sorry about the rubbish title. I wrote the following code, which type checks:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

module Test where

import Data.Kind (Type)

-- Simplification
type family Col (f :: k -> j) (x :: k) :: Type

-- Base types
data PGBaseType = PGInteger | PGText

-- Transformations
data Column t = Column Symbol t
newtype Nullable t = Nullable t
newtype HasDefault t = HasDefault t

-- Interpretations
data Expr k

data Record (f :: forall k. k -> Type) =
  Record {rX :: Col f ('Column "x" 'PGInteger)
         ,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
         ,rZ :: Col f ('HasDefault 'PGText)}

However, if I play with this in GHCI, I can get the following error:

λ> let x = undefined :: Record Expr

<interactive>:136:29-32: error:
    • Expected kind ‘forall k. k -> Type’,
        but ‘Expr’ has kind ‘forall k. k -> *’
    • In the first argument of ‘Record’, namely ‘Expr’
      In an expression type signature: Record Expr
      In the expression: undefined :: Record Expr

It seems that if I write

data Expr :: forall k. k -> Type

things work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.

Change History (3)

comment:1 Changed 4 months ago by RyanGlScott

Luckily, commit a7ee2d4c4229b27af324ebac93081f692835365d (Improve TcFlatten.flattenTyVar) fixed this! I'll add a regression test.

comment:2 Changed 4 months ago by Ryan Scott <ryan.gl.scott@…>

In ba5114e/ghc:

Add regression test for #11966

Commit a7ee2d4c4229b27af324ebac93081f692835365d fixed #11966. Here's a
regression test for it.

comment:3 Changed 4 months ago by RyanGlScott

Milestone: 8.2.1
Resolution: fixed
Status: newclosed
Test Case: dependent/should_compile/T11966
Note: See TracTickets for help on using tickets.