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,242
    • Issues 5,242
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 567
    • Merge requests 567
  • 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
  • #12928
Closed
Open
Issue created 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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking