[GHC] #13655: Spurious untouchable type variable in connection with rank-2 type and constraint family
#13655: Spurious untouchable type variable in connection with rank-2 type and constraint family -------------------------------------+------------------------------------- Reporter: jeltsch | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 (Type checker) | 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 cannot be compiled: {{{#!hs {-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-} import GHC.Exts (Constraint) type family F a b :: Constraint data T b c = T f :: (forall b . F a b => T b c) -> a f _ = undefined }}} GHC outputs the following error message: {{{ Untouchable.hs:9:6: error: • Couldn't match type ‘c0’ with ‘c’ ‘c0’ is untouchable inside the constraints: F a b bound by the type signature for: f :: F a b => T b c0 at Untouchable.hs:9:6-37 ‘c’ is a rigid type variable bound by the type signature for: f :: forall a c. (forall b. F a b => T b c) -> a at Untouchable.hs:9:6 Expected type: T b c0 Actual type: T b c • In the ambiguity check for ‘f’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: f :: (forall b. F a b => T b c) -> a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13655 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13655: Spurious untouchable type variable in connection with rank-2 type and constraint family -------------------------------------+------------------------------------- Reporter: jeltsch | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1-rc2 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Comment (by simonpj): I can see that it seems odd. Imagine that you wrote {{{ f :: (forall b . F a b => T b c) -> a f _ = undefined g :: (forall bb . F aa bb => T bb cc) -> aa g x = f x }}} You'd expect that to work: the two signatures are the same. But in the call in g's rhs we have: {{{ Expected type of f's arg: forall b. F a0 b => T b c0) Actual type of x (after instantation): T bb0 cc plus a "wanted" constraint: F aa bb0 }}} where the "0" things are unification variables. Of course this is easily soluble by unifying `bb0=b, a0=aa, c0=cc`. The `a0=aa` is enforced by the result type of the call to `(f x)` but the other two are not. And the "untouchable" bit is because we don't unify under a given equality constraint, or something that might be a given equality, like `(F a0 b)`. (Why: see the OutsideIn paper.) The ambiguity check, which is failing here, is precisely implementing this reasoning. In short: it's all behaving as designed. The error message is unhelpful, but it IS a subtle issue. I wish I could be more helpful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13655#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC