Re: [GHC] #14046: “Illegal type synonym family application in instance” is too strict in the presence of functional dependencies

[GHC]

#14046: “Illegal type synonym family application in instance” is too strict in the
presence of functional dependencies
-------------------------------------+-------------------------------------
        Reporter:  lexi.lambda       |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #3485             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 > ..., I’m still not completely sure why this wouldn’t be a reasonable
 change.

 Try to figure out the rules:
  * The type family application cannot appear in a 'argument position' of a
 FunDep.
  * There might be multiple FunDeps/multi-directional. (An instance
 parameter might be in 'argument position' by one FunDep, but 'result
 position' from another.)
  * The variables in a type family application must be already bound by
 parameters appearing in 'argument position'. (Or possibly determined from
 those via constraints -- essentially the Liberal Coverage Conditions.)

 It's surely easier to have a blanket rule 'no type families'/achieve the
 effect with equality constraints.

 > The coverage condition itself is precedent for weakening of restrictions
 in the presence of fundeps (in that case, instance decidability), and this
 does not seem meaningfully different to me.

 Even `UndecidableInstances` doesn't allow complete chaos. If that's what
 you want, there's a feature request somewhere dubbed 'dysfunctional
 functional dependencies'.

 > I could be convinced by an example of the sort that SPJ alluded to, ...

 First consider type synonyms appearing in instance heads:

 {{{
 {-# LANGUAGE FlexibleInstances #-}

 instance Multi String String where ...

 -- immediately expanded to

 instance Multi [Char] [Char] where ...

 -- not: instance (b0 ~ [Char]) => Multi [Char] b0
 }}}

 OK Let's try to concoct an example per SPJ. Suppose

 {{{
 type family Fam a where
   Fam a = Int

 instance Multi (Maybe a) (Fam a) where ...

 -- immediately expanded to

 instance Multi (Maybe a) Int where ...
 }}}

 At the use site, GHC will wait until `b` is resolved to `Int` before it
 will use the instance.

 > ... in which an instance of the form Multi X (Y a) behaves differently
 from (b ~ Y a) => Multi X b, but I’m not sure sure what such an example
 would look like or how it would differ from a user’s point of view.

 You mean `Y` is a type family? I'm not seeing that `instance Multi X (Y
 a)` would ever be a good idea: there's nothing to tell what `a` is. Even
 if the use site tells `Y a ~ Int`, that's no help (unless `Y` is injective
 -- but that's a different scenario).

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14046#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler