Re: [GHC] #14840: QuantifiedConstraints: Can't define class alias

23 Feb 2018

      #14840: QuantifiedConstraints: Can't define class alias
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints wipT2893
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I'm not sure that this is a bug. Here's a reduced version of your first
 program:

 {{{#!hs
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 data T a

 class C1 a

 class    (forall a. cls (T a)) => C2 cls
 instance (forall a. cls (T a)) => C2 cls
 }}}

 Note that this works without `PolyKinds`, which should give you an idea of
 the underlying issue. If you compile this with `-fprint-explicit-kinds`,
 the error message is more enlightening:

 {{{
 Bug.hs:12:10: error:
     • Could not deduce: cls (T k0 a)
       from the context: forall (a :: k). cls (T k a)
         bound by an instance declaration:
                    forall k (cls :: * -> Constraint).
                    (forall (a :: k). cls (T k a)) =>
                    C2 cls
         at Bug.hs:12:10-40
     • In the ambiguity check for an instance declaration
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the instance declaration for ‘C2 cls’
    |
 12 | instance (forall a. cls (T a)) => C2 cls
    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 You can fix this by explicitly binding the kind of `a`:

 {{{#!hs
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 data T a

 class C1 a

 class    (forall k (a :: k). cls (T a)) => C2 cls
 instance (forall k (a :: k). cls (T a)) => C2 cls
 }}}

 With that in mind, here's the fixed version of your first program:

 {{{#!hs
 {-# Language TypeInType, MultiParamTypeClasses, TypeFamilies,
 FlexibleContexts, FunctionalDependenc
 ies, AllowAmbiguousTypes, QuantifiedConstraints, GADTs, ConstraintKinds,
 KindSignatures, RankNTypes
 , FlexibleInstances, UndecidableInstances, TypeOperators #-}

 import Data.Kind

 class Reifies s a | s -> a where
   reflect :: proxy s -> a

 newtype Lift :: forall k. (Type -> Constraint) -> Type -> k -> Type where
   Lift :: a -> Lift cls a s

 data family Def :: (k -> Constraint) -> (k -> Type)

 class    (forall k (s :: k) a. Reifies s (Def cls a) => cls (Lift cls a
 s)) => ReifiableConstraint
 cls
 instance (forall k (s :: k) a. Reifies s (Def cls a) => cls (Lift cls a
 s)) => ReifiableConstraint
 cls
 }}}

 The program in comment:1 seems to be of an entirely different nature.

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