Skip to content

Type checking with PartialTypeSignatures is broken

Steps to reproduce

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE BlockArguments #-}

import Control.Exception

data Foo = Foo
  deriving (Show, Exception)

class CanThrow e

qux :: Monad m => (CanThrow Foo => m a) -> m a
qux _ = undefined

class Monad m => MonadCheckedThrow m where
    throwChecked :: (Exception e, CanThrow e) => e -> m a

foo :: MonadCheckedThrow m => m Int
foo = do
  qux do
    _ <- baz
    pure 5
  where
    baz :: (CanThrow Foo, _) => _
    baz = throwChecked Foo
error:
    • Could not deduce (CanThrow Foo)
      from the context: MonadCheckedThrow m
        bound by the type signature for:
                   foo :: forall (m :: * -> *). MonadCheckedThrow m => m Int
        at _
      or from: MonadCheckedThrow m1
        bound by the inferred type for ‘baz’:
                   forall (m1 :: * -> *) a. MonadCheckedThrow m1 => m1 a
        at _
    • When checking that the inferred type
        baz :: forall (m :: * -> *) a.
               (CanThrow Foo, MonadCheckedThrow m) =>
               m a
      is as general as its (partial) signature
        baz :: forall (m :: * -> *) a. MonadCheckedThrow m => m a
      In an equation for ‘foo’:
          foo
            = do qux
                   do _ <- baz
                      ....
            where
                baz :: (CanThrow Foo, _) => _
                baz = throwChecked Foo

Expected behavior

GHC must check bar's type.
By the way the following code is checked:

baz :: (c ~ CanThrow, c Foo, _) => _
baz = throwChecked Foo
-- and
baz :: (f ~ Foo, CanThrow f, _) => _
baz = throwChecked Foo
-- and even
baz :: _ => CanThrow Foo => _
baz = throwChecked Foo

Environment

  • GHC version used: 8.10.7
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information