I'm not particularly wedded to whether I use
{{{#!hs type family Gcd :: Nat -> Nat -> Nat }}}
or
{{{#!hs type family Gcd (n:: Nat) (m::Nat) :: Nat }}}
here.
The one thing I have in favor (or against, depending on your
#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 adamgundry): Replying to [comment:30 ekmett]: perspective) of the Nat -> Nat -> Nat encoding is that it allows me to preclude the user actually defining any ad hoc base cases. Switching to the other address the "eta" concern to some extent. Doesn't an empty closed type family serve the same purpose? The first encoding seems simply wrong, because it implies that `Gcd` is injective. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler