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,842
    • Issues 4,842
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 457
    • Merge requests 457
  • 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
  • #18645

Closed
Open
Created Sep 03, 2020 by Sebastian Graf@sgraf812Developer

Incremental `tcCheckSatisfiability` API

The pattern-match checker makes use of the function tcCheckSatisfiability :: Bag EvVar -> TcM Bool (henceforth tcCS) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a Bag EvVar is accumulated and incrementally checked after each addition. As #17836 (closed) shows in a rather painful way, that scales quadratically, because the type-checker chews through the same type constraints over and over again.

But look at how the pattern-match checker uses tcCS:

-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
  = do { evs <- traverse nameTyCt cts
       ; let new_inert = inert `unionBags` evs
       ; ... <- initTcDsForSolver $ tcCheckSatisfiability new_inert
       ; ... }

The inert set is a Bag EvVar for which we already know they are compatible with each other, as they were checked by tcCS in a previous call. Only cts :: Bag PredType are unchecked. And as far as the pattern-match checker is concerned, the type of inert is completely opaque, so the API to tcCS could very well be

tcCheckSatisfiability :: TcInert -> Bag EvVar -> TcM (Maybe TcInert)

-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
  = do { evs <- traverse nameTyCt cts
       ; ...mb_new_inert... <- initTcDsForSolver $ tcCheckSatisfiability inert evs
       ; ... }

I'm sure there already is something like TcInert in the type-checker. Looking at the implementation of tcCS, that might be the unused EvBindMap, but I'm not sure. Or is it the InertCans in getInertCans/setInertCans? CC @rae, @RyanGlScott, @simonpj

This blocks #17836 (closed) and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.

Edited Sep 03, 2020 by Sebastian Graf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking