[GHC] #14968: QuantifiedConstraints: Can't be RHS of type family instances

24 Mar 2018

      #14968: QuantifiedConstraints: Can't be RHS of type family instances
-------------------------------------+-------------------------------------
           Reporter:  josef          |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here's a type family that I tried to write using QuantifiedConstraints.

 {{{#!hs
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 module QCTypeInstance where

 import GHC.Exts (Constraint)

 type family   Functors (fs :: [(* -> *) -> * -> *]) :: Constraint
 type instance Functors '[] = (() :: Constraint)
 type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f),
 Functors ts)
 }}}

 Unfortunately, GHC complains that it's illegal to have polymorphism on the
 right hand side of a type instance definition.

 {{{
 $ ../ghc-wip/T2893/inplace/bin/ghc-stage2 --interactive QCTypeInstance.hs
 GHCi, version 8.5.20180322: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling QCTypeInstance   ( QCTypeInstance.hs, interpreted )

 QCTypeInstance.hs:13:15: error:
     • Illegal polymorphic type:
         forall (f :: * -> *). Functor f => Functor (t f)
     • In the type instance declaration for ‘Functors’
    |
 13 | type instance Functors (t ': ts) = (forall f. Functor f => Functor (t
 f), Functors ts)
    |               ^^^^^^^^
 }}}

 Would it be possible to lift this restriction and allow quantified
 constraints as right hand sides of type family instances? Or are there
 fundamental difficulties with what I'm trying to do?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler