Subvert your type checker today!

Motivation

Gabe Dijkstra’s Haskell eXchange 2018 talk showed how we can write extensions to GHC’s type checking via plugins. The sky is the limit!

Do you wish you could do IO from any monad transformer stack, including those stacks that do not have IO at the base? Do you think RIO is an interesting concept, but would rather just do IO from your regular ol’ Reader computations? Prefer writing pure code in the Identity monad for the sake of do-notation but still want to do some IO in there? Are you frustrated when you have to propagate MonadIO constraints throughout a ladder of function calls?

Then this post is for you!

Extending the Type Checker

Gabe Dijkstra’s slides from his talk break down how to build a type checker plugin. We won’t rehash everything Gabe explains in this blog post. Instead, we’ll get on with writing a plugin right away.

Our module will export the required plugin binding. We name it TcYolo to indicate to our users that it is a reliable type checker plugin and very suitable for production use cases.

module TcYolo
  ( plugin
  ) where

Ye olde wall o’ imports - note that we’ll need the ghc library for some of these:

import Class (className)
import Control.Monad (guard)
import Data.Maybe (mapMaybe)
import OccName (HasOccName(occName), mkClsOcc)
import Plugins (Plugin, defaultPlugin, tcPlugin)
import TcEvidence (EvTerm)
import TcRnTypes
  ( TcPlugin(TcPlugin, tcPluginInit, tcPluginSolve, tcPluginStop),
  , TcPluginResult(TcPluginOk), Ct, ctEvPred, ctEvTerm, ctEvidence
  )
import Type (PredTree(ClassPred), classifyPredType)

The exported type checker plugin:

plugin :: Plugin
plugin = defaultPlugin
  { tcPlugin = const . pure $ TcPlugin
    { tcPluginInit = pure ()
    , tcPluginStop = const (pure ())
    , tcPluginSolve = \() _givenCts _derivedCts wantedCts ->
        pure . TcPluginOk (mapMaybe solveMonadIOCt wantedCts) $ []
    }
  }

And finally the constraint solver for what our plugin cares about - solving the MonadIO constraint anywhere our users’ code wants it!

solveMonadIOCt :: Ct -> Maybe (EvTerm, Ct)
solveMonadIOCt ct = do
  ClassPred cls _types <- pure . classifyPredType . ctEvPred . ctEvidence $ ct
  guard (mkClsOcc "MonadIO" == occName (className cls))
  -- The first part of this pair is probably wrong? ¯\_(ツ)_/¯
  pure (ctEvTerm . ctEvidence $ ct, ct)

Using the Plugin

We can use the plugin via the -fplugin GHC option:

{-# OPTIONS_GHC -fplugin=TcYolo #-}

module TcYoloExample
  ( whereIsYourGodNow
  , noneShallPass
  , becauseWhyNot
  ) where

import Control.Monad.IO.Class (MonadIO(liftIO))
import Control.Monad.Trans.Except (Except)
import Control.Monad.Trans.Reader (Reader)
import Control.Monad.Trans.State (StateT, get)
import Data.Functor.Identity (Identity)
import System.IO.Error (userError)
import System.Random (Random(randomIO))

whereIsYourGodNow :: Reader () Int
whereIsYourGodNow = liftIO randomIO

noneShallPass :: Identity ()
noneShallPass = liftIO . ioError . userError $ "blah"

becauseWhyNot :: StateT Int (Except String) Int
becauseWhyNot = do
  fileLength <- fmap length (liftIO . readFile $ "some-file.txt")
  extraLength <- get
  pure $ fileLength + extraLength

-- Note that the above code typechecks, but termination is a different story! 😛

The plugin and example code are available in a repo here.