GitLab

With Simon's latest changes (ticket:14733##14832) this works:

{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-}

import Control.Category
import Data.Kind
import Data.Coerce

data With cls a b where
  With :: cls a b => With cls a b

type Coercion = With Coercible

type Refl  rel = (forall xx.       rel xx xx :: Constraint)
type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint)

instance Refl rel => Category (With rel) where
  id = With
  (.) = undefined

But strengthening the context with Trans rel:

instance (Refl rel, Trans rel) => Category (With rel) where

causes it to fail

GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( J.hs, interpreted )

J.hs:15:10: error:
    • Could not deduce: rel xx zz
      from the context: (Refl rel, Trans rel)
        bound by an instance declaration:
                   forall k (rel :: k -> k -> Constraint).
                   (Refl rel, Trans rel) =>
                   Category (With rel)
        at J.hs:15:10-53
      or from: (rel xx yy, rel yy zz)
        bound by a quantified context at J.hs:15:10-53
    • In the ambiguity check for an instance declaration
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the instance declaration for ‘Category (With rel)’
   |
15 | instance (Refl rel, Trans rel) => Category (With rel) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

J.hs:15:10: error:
    • Could not deduce: rel xx xx
      from the context: (Refl rel, Trans rel)
        bound by an instance declaration:
                   forall k (rel :: k -> k -> Constraint).
                   (Refl rel, Trans rel) =>
                   Category (With rel)
        at J.hs:15:10-53
    • In the ambiguity check for an instance declaration
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the instance declaration for ‘Category (With rel)’
   |
15 | instance (Refl rel, Trans rel) => Category (With rel) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude> 

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture