Opened 3 years ago

Closed 3 years ago

#12845 closed bug (fixed)

-XPartialTypeSignatures results in unbound variables

Reported by: crockeea Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: partial-sigs/should_compile/T12845
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (3)

comment:1 Changed 3 years ago by RyanGlScott

If I'm reading this right, this appears to work in GHC HEAD:

$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.1.20161010: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:16:70: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘() :: Constraint’
    • In the type signature:
        broken :: forall r r' rngs.
                  ('(r, r') ~ Head rngs, Bar r r' ~ True, _) =>
                  Foo r -> Proxy rngs -> ()
Ok, modules loaded: Main.

comment:2 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 83a952d1/ghc:

Test Trac #12845

comment:3 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: partial-sigs/should_compile/T12845

I don't quite know what fixed this, and I suspect it'll be hard to get into 8.0, so I'll just close this.

Note: See TracTickets for help on using tickets.