-XPartialTypeSignatures results in unbound variables

The following code fails to compile, but I think it should.

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

import Data.Proxy

data Foo (m :: Bool)

type family Head (xs :: [(Bool, Bool)]) where Head (x ': xs) = x

type family Bar (x :: Bool) (y :: Bool) :: Bool

-- to trigger the bug, r and r' cannot *both* appear on the RHS
broken :: forall r r' rngs . ('(r,r') ~ Head rngs, Bar r r' ~ 'True, _)
  => Foo r -> Proxy rngs -> ()
broken x _ = let y = requireBar x :: Foo r' in ()

requireBar :: (Bar m m' ~ 'True) => Foo m -> Foo m'
requireBar = undefined

The error is:

> ghci UnboundVar.hs 
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( UnboundVar.hs, interpreted )

UnboundVar.hs:18:1: error:
    • Could not deduce: Bar r r'0 ~ 'True
      from the context: ('(r, r') ~ Head rngs,
                         Bar r r' ~ 'True,
                         Bar r r' ~ 'True)
        bound by the inferred type for ‘broken’:
                   ('(r, r') ~ Head rngs, Bar r r' ~ 'True, Bar r r' ~ 'True) =>
                   Foo r -> Proxy rngs -> ()
        at UnboundVar.hs:18:1-49
      The type variable ‘r'0’ is ambiguous
    • When checking that the inferred type
        broken :: forall (r :: Bool) (r' :: Bool) (rngs :: [(Bool, Bool)]).
                  Bar r r' ~ 'True =>
                  Foo r -> Proxy rngs -> ()
      is as general as its (partial) signature
        broken :: forall (r :: Bool) (r' :: Bool) (rngs :: [(Bool, Bool)]).
                  ('(r, r') ~ Head rngs, Bar r r' ~ 'True, Bar r r' ~ 'True) =>
                  Foo r -> Proxy rngs -> ()

If I remove the partial type signature (i.e., remove the _ constraint from broken), then GHC happily accepts the code. I'm not sure why adding a _ introduces ambiguity; it seems GHC is forgetting that r' is bound by the forall (and that -XScopedTypeVariables is enabled).

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture