Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,830
    • Issues 4,830
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 447
    • Merge requests 447
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #13761

Closed
Open
Created May 27, 2017 by Ryan Scott@RyanGlScottMaintainer

Can't create poly-kinded GADT with TypeInType enabled, but can without

Surprisingly, this compiles without TypeInType:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Works where

import Data.Kind

data T :: k -> Type where
  MkT :: T Int

But once you add TypeInType:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

data T :: k -> Type where
  MkT :: T Int

then it stops working!

GHCi, version 8.3.20170516: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:11:12: error:
    • Expected kind ‘k’, but ‘Int’ has kind ‘*’
    • In the first argument of ‘T’, namely ‘Int’
      In the type ‘T Int’
      In the definition of data constructor ‘MkT’
   |
11 |   MkT :: T Int
   |            ^^^

This bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.

What's strange about this bug is that is requires that you write T with an explicit kind signature. If you write T like this:

data T (a :: k) where
  MkT :: T Int

Then it will work with TypeInType enabled.

Trac metadata
Trac field Value
Version 8.0.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking