#12845: -XPartialTypeSignatures results in unbound variables -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12845 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler