Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,322
    • Issues 4,322
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 368
    • Merge Requests 368
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #12928

Closed
Open
Opened Dec 05, 2016 by Vladislav Zavialov@int-indexDeveloper

Too easy to trigger CUSK condition using TH

While trying to make singletons class promotion work with kind-polymorphic type variables, I've encountered a problem regarding CUSKs.

Consider this class:

$(promoteOnly [d|
  class Cls a  where
    fff :: Proxy a -> ()
  |])

The generated TH (slightly simplified by hand) looks like this:

type FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm

data FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ())

type instance Apply FffSym0 l_alvn = FffSym1 l_alvn

class PCls a_alve where
  type Fff (arg_alvl :: Proxy a_alve) :: ()

However, it fails to compile with the following error:

cusk.hs:25:1: error:
    You have written a *complete user-suppled kind signature*,
    but the following variable is undetermined: k0 :: *
    Perhaps add a kind signature.
    Inferred kinds of user-written variables:
      a1627472612 :: k0
      l_alvn :: TyFun (Proxy a1627472612) ()

As suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write

data FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ())

and it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so.

Looking at the module TcHsType in the GHC sources, I see that the error is reported by the kcHsTyVarBndrs function:

          -- If there are any meta-tvs left, the user has
          -- lied about having a CUSK. Error.
       ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
       ; when (not (null meta_tvs)) $
         report_non_cusk_tvs (qkvs ++ tc_tvs)

However, I don't see why we can't generalize over meta_tvs instead of reporting a failure. I asked on IRC #ghc and ezyang suggested that it should be sound.

Below I attach a self-contained example that demonstrates the issue and has no dependencies except base.

Trac metadata
Trac field Value
Version 8.0.1
Type FeatureRequest
TypeOfFailure OtherFailure
Priority high
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#12928