#10493: Inaccessible code might be accessible with newtypes and Coercible -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): That's the right place. Currently we have {{{ -- Fail straight away for better error messages -- See Note [Use canEqFailure in canDecomposableTyConApp] | isDataFamilyTyCon tc1 || isDataFamilyTyCon tc2 = canEqFailure ev eq_rel ty1 ty2 | otherwise = canEqHardFailure ev eq_rel ty1 ty2 }}} I think you are proposing {{{ | eq_rel == ReprEq && not (isDistinctTyCon tc1 && isDictinctTyCon tc2) = canEqFailure ev eq_rel ty1 ty2 | otherwise = canEqHardFailure ev eq_rel ty1 ty2 }}} That looks right, given the comment on `isDistinctTyCon`: {{{ -- | 'isDistinctTyCon' is true of 'TyCon's that are equal only to -- themselves, even via coercions (except for unsafeCoerce). -- This excludes newtypes, type functions, type synonyms. -- It relates directly to the FC consistency story: -- If the axioms are consistent, -- and co : S tys ~ T tys, and S,T are "distinct" TyCons, -- then S=T. }}} Tihs comment is vague about roles. If we have a poof co :: S ~r T, and S and T are "distinct" then S=T. But at what role is 'r'? It would be helpful to clarify this comment in role vocabulary. Similarly the comment `Note [Pruning dead case alternatives]` in `Unify.hs` needs reviewing in the role world. `Unify.typesCantMatch` is basically checking for apartness; which is also implemented somehwere else. Can we combine? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10493#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10493: Inaccessible code might be accessible with newtypes and Coercible -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Replying to [comment:3 goldfire]:

It would be nice to combine `typesCantMatch` with the apartness check, but there's a key difference: `typesCantMatch` is about representational equality, but apartness is about nominal equality.

I don't agree at all! If you look at the single call to `typesCantMatch` you'll see that it's passed a list of '''Nominal''' equalities, namely the ones bound by the GADT. Admittedly this is not documented, and it should be. But it's true. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10493#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10493: Inaccessible code might be accessible with newtypes and Coercible -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: merge Priority: normal | Milestone: 7.10.3 Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | typecheck/should_compile/T10493 | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => typecheck/should_compile/T10493 * milestone: => 7.10.3 Old description:

If I say

{{{ module A (Age, ageCo) where

import Data.Type.Coercion

newtype Age = MkAge Int

ageCo :: Coercion Age Int ageCo = Coercion }}}

{{{ {-# LANGUAGE FlexibleContexts #-}

module B where

import Data.Coerce import A

foo :: Coercible Age Int => () foo = () }}}

I get

{{{ B.hs:8:8: error: Couldn't match representation of type ‘Age’ with that of ‘Int’ Inaccessible code in the type signature for: foo :: Coercible Age Int => () In the ambiguity check for the type signature for ‘foo’: foo :: Coercible Age Int => () To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘foo’: foo :: Coercible Age Int => () }}}

I agree that module `B` can't directly prove `Coercible Age Int`. But `ageCo` is in scope which proves exactly this! So it is provable, albeit directly. GHC should not claim that the code is inaccessible.

Proposed fix: in `canDecomposableTyConApp`, only call `canEqHardFailure` for a representational equality when both tycons involved say `True` to `isDistinctTyCon`.

I'm happy to put the fix in, once someone seconds this idea. Getting this right has proved harder than I thought!

New description: If I say {{{ module A (Age, ageCo) where import Data.Type.Coercion newtype Age = MkAge Int ageCo :: Coercion Age Int ageCo = Coercion }}} {{{ {-# LANGUAGE FlexibleContexts #-} module B where import Data.Coerce import A foo :: Coercible Age Int => () foo = () }}} I get {{{ B.hs:8:8: error: Couldn't match representation of type ‘Age’ with that of ‘Int’ Inaccessible code in the type signature for: foo :: Coercible Age Int => () In the ambiguity check for the type signature for ‘foo’: foo :: Coercible Age Int => () To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘foo’: foo :: Coercible Age Int => () }}} I agree that module `B` can't directly prove `Coercible Age Int`. But `ageCo` is in scope which proves exactly this! So it is provable, albeit indirectly. GHC should not claim that the code is inaccessible. Proposed fix: in `canDecomposableTyConApp`, only call `canEqHardFailure` for a representational equality when both tycons involved say `True` to `isDistinctTyCon`. I'm happy to put the fix in, once someone seconds this idea. Getting this right has proved harder than I thought! -- Comment: Merge if convenient. This is a real bug, but it's somewhat obscure. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10493#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10493: Inaccessible code might be accessible with newtypes and Coercible -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 7.10.3 Component: Compiler | Version: 7.10.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T10493 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: This has been merged to `ghc-7.10` as 5df26ae. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10493#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10493: Inaccessible code might be accessible with newtypes and Coercible -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 7.10.3 Component: Compiler | Version: 7.10.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T10493 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): I was able to cherry-pick 228ddb95ee137e7cef02dcfe2521233892dd61e0 to `ghc-7.10`. Unfortunately ff82387d6fe61762fe4f507e8f9799f5bdc3c43a appears to depend upon the superclass rework so I think I'll just have to punt on all of this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10493#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler