Created
February 7, 2020 21:32
-
-
Save parsonsmatt/ab90807f1d14d750720b59173f2052fe to your computer and use it in GitHub Desktop.
What's goin on with my skolems
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- This reproduction can be played with using `ghcid --allow-eval` | |
{-# language RankNTypes #-} | |
import Control.Monad.ST | |
newtype IdT m a = IdT { unIdT :: m a } | |
-- $> :set -XRankNTypes | |
-- | |
-- @jkachmar pointed this out to me, and I'm at a loss. If we pattern match | |
-- directly on the `IdT` transformer, then the result value results in the | |
-- @s@ type variable escaping somehow. | |
-- | |
-- $> :t (\(IdT x) -> runST x) :: (forall s. IdT (ST s) a) -> a | |
-- | |
-- <interactive>:1:21: error: | |
-- • Couldn't match type ‘s’ with ‘s0’ | |
-- ‘s’ is a rigid type variable bound by | |
-- a type expected by the context: | |
-- forall s. ST s a1 | |
-- at <interactive>:1:15-21 | |
-- Expected type: ST s a1 | |
-- Actual type: ST s0 a1 | |
-- • In the first argument of ‘runST’, namely ‘x’ | |
-- In the expression: runST x | |
-- In the expression: | |
-- (\ (IdT x) -> runST x) :: (forall s. IdT (ST s) a) -> a | |
-- • Relevant bindings include | |
-- x :: ST s0 a1 (bound at <interactive>:1:8) | |
-- | |
-- | |
-- But this one works just fine, using the runner function. | |
-- | |
-- $> :t (\a -> runST (unIdT a)) :: (forall s. IdT (ST s) a) -> a | |
-- | |
-- What gives? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment