Skip to content
GitLab
Projects Groups Snippets
  • /
  • 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 5,259
    • Issues 5,259
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 564
    • Merge requests 564
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14515
Closed
Open
Issue created Nov 23, 2017 by Icelandjack@IcelandjackReporter

"Same" higher-rank kind synonyms behave differently

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
Trac metadata
Trac field Value
Version 8.2.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
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