-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 |