Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

6 Nov 2017

      #11066: Inacessible branch should be warning - otherwise breaks type soundness?
-------------------------------------+-------------------------------------
        Reporter:  rrnewton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #8128, #8740      |  Differential Rev(s):  Phab:D1454
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by dfeuer):

 Here's a much smaller reproduction of what I suspect is going on in
 Edward's code:

 {{{#!hs
 {-# language DataKinds #-}
 {-# language TypeFamilies #-}
 {-# language TypeOperators #-}
 module T11066 where
 import Data.Type.Equality
 import GHC.TypeLits (Nat)

 type family Gcd :: Nat -> Nat -> Nat

 foo :: 1 :~: Gcd 3 4 -> ()
 foo Refl = ()
 }}}

 This produces

 {{{
 T11066.hs:11:5: error:
     • Couldn't match type ‘Gcd 3 4’ with ‘1’
       Inaccessible code in
         a pattern with constructor: Refl :: forall k (a :: k). a :~: a,
         in an equation for ‘foo’
     • In the pattern: Refl
       In an equation for ‘foo’: foo Refl = ()
    |
 11 | foo Refl = ()
    |
 }}}

 even though someone could easily `unsafeCoerce` their way into `1 :~: Gcd
 3 4`. My hypothesis about the type family is supported by the fact that
 changing `Gcd` to

 {{{#!hs
 type family Gcd (a :: Nat) (b :: Nat) :: Nat
 }}}

 makes the problem go away. But I suspect ekmett needs the original version
 to be able to perform symbolic calculations on `Gcd`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:24
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler