[GHC] #14878: Can't witness transitivity ((.)) of isomorphism of Constraints

2 Mar 2018


      #14878: Can't witness transitivity ((.)) of isomorphism of Constraints
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints, wipT2893    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This compiles,

 {{{#!hs
 {-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators,
 FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}

 data Dict c where
   Dict :: c => Dict c

 class    (a => b) => Implies a b
 instance (a => b) => Implies a b

 type a -:- b = Dict (Implies a b, Implies b a) -- isomorphism of
 constraints, should be an equivalence relation

 id_ :: a-:-a
 id_ = Dict

 sym_ :: a-:-b -> b-:-a
 sym_ Dict = Dict

 -- comp_ :: a-:-b -> b-:-c -> a-:-c
 -- comp_ Dict Dict = Dict
 }}}

 but uncommenting `comp_` and GHC doesn't know how to deduce `b` (the
 location message is weird)

 {{{
 $ ghci -ignore-dot-ghci hs/206-bug-quantified-constraints.hs
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( hs/206-bug-quantified-
 constraints.hs, interpreted )

 hs/206-bug-quantified-constraints.hs:1:1: error:
     Could not deduce: b
     from the context: (Implies a b, Implies b a)
       bound by a pattern with constructor:
                  Dict :: forall (c :: Constraint). c => Dict c,
                in an equation for ‘comp_’
       at hs/206-bug-quantified-constraints.hs:18:7-10
     or from: (Implies b c, Implies c b)
       bound by a pattern with constructor:
                  Dict :: forall (c :: Constraint). c => Dict c,
                in an equation for ‘comp_’
       at hs/206-bug-quantified-constraints.hs:18:12-15
     or from: c
       bound by a quantified context
       at hs/206-bug-quantified-constraints.hs:1:1
   |
 1 | {-# Language QuantifiedConstraints, GADTs, ConstraintKinds,
 TypeOperators, FlexibleInstances, MultiParamTypeClasses,
 UndecidableInstances #-}
   | ^

 hs/206-bug-quantified-constraints.hs:1:1: error:
     Could not deduce: b
     from the context: (Implies a b, Implies b a)
       bound by a pattern with constructor:
                  Dict :: forall (c :: Constraint). c => Dict c,
                in an equation for ‘comp_’
       at hs/206-bug-quantified-constraints.hs:18:7-10
     or from: (Implies b c, Implies c b)
       bound by a pattern with constructor:
                  Dict :: forall (c :: Constraint). c => Dict c,
                in an equation for ‘comp_’
       at hs/206-bug-quantified-constraints.hs:18:12-15
     or from: a
       bound by a quantified context
       at hs/206-bug-quantified-constraints.hs:1:1
   |
 1 | {-# Language QuantifiedConstraints, GADTs, ConstraintKinds,
 TypeOperators, FlexibleInstances, MultiParamTypeClasses,
 UndecidableInstances #-}
   | ^
 Failed, no modules loaded.
 Prelude>
 }}}

 simplifying and uncurrying we get a more minimal example

 {{{#!hs
 {-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators,
 FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}

 data Dict c where
   Dict :: c => Dict c

 f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
 f = Dict
 }}}

 giving a different and longer error message

 {{{
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 206-bug-quantified-constraints.hs,
 interpreted )

 206-bug-quantified-constraints.hs:6:6: error:
     • Could not deduce: c0
       from the context: (a => b, b => a, b => c, c => b, a => c, c)
         bound by the type signature for:
                    f :: forall (a :: Constraint) (b :: Constraint) (c ::
 Constraint).
                         (a => b, b => a, b => c, c => b, a => c, c) =>
                         Dict a
         at 206-bug-quantified-constraints.hs:6:6-58
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |
 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 206-bug-quantified-constraints.hs:6:6: error:
     • Could not deduce: (b, c0)
       from the context: (a => b, b => a, b => c, c => b, a => c, c)
         bound by the type signature for:
                    f :: forall (a :: Constraint) (b :: Constraint) (c ::
 Constraint).
                         (a => b, b => a, b => c, c => b, a => c, c) =>
                         Dict a
         at 206-bug-quantified-constraints.hs:6:6-58
       or from: a
         bound by a quantified context
         at 206-bug-quantified-constraints.hs:6:6-58
     • In the type signature:
         f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |
 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 206-bug-quantified-constraints.hs:6:6: error:
     • Could not deduce: b0
       from the context: (a => b, b => a, b => c, c => b, a => c, c)
         bound by the type signature for:
                    f :: forall (a :: Constraint) (b :: Constraint) (c ::
 Constraint).
                         (a => b, b => a, b => c, c => b, a => c, c) =>
                         Dict a
         at 206-bug-quantified-constraints.hs:6:6-58
       or from: c0
         bound by a quantified context
         at 206-bug-quantified-constraints.hs:6:6-58
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |
 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 206-bug-quantified-constraints.hs:6:6: error:
     • Could not deduce: c0
       from the context: (a => b, b => a, b => c, c => b, a => c, c)
         bound by the type signature for:
                    f :: forall (a :: Constraint) (b :: Constraint) (c ::
 Constraint).
                         (a => b, b => a, b => c, c => b, a => c, c) =>
                         Dict a
         at 206-bug-quantified-constraints.hs:6:6-58
       or from: b0
         bound by a quantified context
         at 206-bug-quantified-constraints.hs:6:6-58
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |
 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 206-bug-quantified-constraints.hs:6:6: error:
     • Could not deduce: b
       from the context: (a => b, b => a, b => c, c => b, a => c, c)
         bound by the type signature for:
                    f :: forall (a :: Constraint) (b :: Constraint) (c ::
 Constraint).
                         (a => b, b => a, b => c, c => b, a => c, c) =>
                         Dict a
         at 206-bug-quantified-constraints.hs:6:6-58
       or from: b0
         bound by a quantified context
         at 206-bug-quantified-constraints.hs:6:6-58
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |
 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 206-bug-quantified-constraints.hs:6:6: error:
     • Could not deduce: (b, b0)
       from the context: (a => b, b => a, b => c, c => b, a => c, c)
         bound by the type signature for:
                    f :: forall (a :: Constraint) (b :: Constraint) (c ::
 Constraint).
                         (a => b, b => a, b => c, c => b, a => c, c) =>
                         Dict a
         at 206-bug-quantified-constraints.hs:6:6-58
       or from: a
         bound by a quantified context
         at 206-bug-quantified-constraints.hs:6:6-58
     • In the type signature:
         f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |
 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Failed, no modules loaded.
 Prelude>
 }}}

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