Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

#14822 closed bug (invalid)

-XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>)

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This code works fine:

{-# Language TypeOperators, RankNTypes, KindSignatures, GADTs, DataKinds, MultiParamTypeClasses, FlexibleInstances, ConstraintKinds, ScopedTypeVariables #-}

import Data.Kind

-- 'constraints' machinery
data Dict c where
  Dict :: c => Dict c

newtype a :- b = Sub (a => Dict b) -- entailment

-- 'singletons' machinery
data SBool :: Bool -> Type where
  SFalse :: SBool 'False
  STrue  :: SBool 'True

class    SBoolI (bool::Bool) where sbool :: SBool bool
instance SBoolI 'False       where sbool = SFalse
instance SBoolI 'True        where sbool = STrue

-- VVV Example VVV
class    Funny (b::Bool) (b'::Bool)
instance Funny 'False b'
instance Funny 'True  'True
instance Funny 'True  'False

proof :: forall b b'. (SBoolI b, SBoolI b') :- Funny b b'
proof = Sub (case (sbool :: SBool b, sbool :: SBool b') of
  (SFalse, _)      -> Dict
  (STrue,  SFalse) -> Dict 
  (STrue,  STrue)  -> Dict)
-- ^^^ Example ^^^

What I'm interested in is the entailment:

Singletons for b and b' entail Funny b b'. This is witnessed by proof.

Given that we have a branch for -XQuantifiedConstraints, it is tantalizing to convert this into an implication constraint (SBoolI b, SBoolI b') => Funny b b'.

Is such a thing sensible (wrt coherence) and if so is it at all possible to do this on WIPT2893?

Change History (5)

comment:1 Changed 19 months ago by kcsongor

What would the conditions of generating such an implication constraint be?

To me it seems like this would make use of the fact that the kind Bool is closed, and in theory, a constraint forall (b :: Bool). C b could be discharged by having individual instances for C 'True and C 'False. Or in terms of implication constraints, that forall (b :: Bool). C b => D b could be built from the individual constituents.

If my understanding is correct as written above, then I don't think it would make sense.

When I see a quantified implication constraint, like forall a. C a => D a, I expect it to be parametric in a, which means that the solution of that constraint should be a function that uses the dictionary for C a to build the dictionary for D a, regardless of what a is instantiated to. (This expectation is grounded in the open world assumption.)

For what it's worth, I think the question can be reformulated as whether the constraint (forall a b. Funny a b) should be solved based on your provided instances (to which I would answer no).

Last edited 19 months ago by kcsongor (previous) (diff)

comment:2 Changed 19 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

I fully agree with kcsongor's analysis. This is essentially asking for a way to violate the open-world assumption, which isn't going to fly. If you want to use (SBoolI b, SBoolI b') => Funny b b' as a quantified constraint, then write an instance for it.

comment:3 Changed 18 months ago by Iceland_jack

I claim I don't rely on Bool being closed. I wouldn't expect forall b. C b to be resolved, it is more like pi b. C b (forall b. SBoolI b => C b) which is subtly different.

Instead I ultimately rely on SBool being closed. I found a way to emulate this with unsafeCoerce. Here is an example for the open kind Type:

{-# Language KindSignatures, GADTs, ConstraintKinds, QuantifiedConstraints, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, RankNTypes #-}

import Data.Kind
import Unsafe.Coerce

-- constraints
data Dict :: Constraint -> Type where
  Dict :: c => Dict c

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

type a |- b = Dict (a `Implies` b)

-- Representation of two types: Int and Bool
data S :: Type -> Type where
  SInt  :: S Int
  SBool :: S Bool

-- Can be passed implicitly
class    SI a    where s :: S a
instance SI Int  where s = SInt
instance SI Bool where s = SBool

-- Can be eliminated with an if-then-else
sElim :: S a -> (Int ~ a => res) -> (Bool ~ a => res) -> res
sElim SInt  i _ = i
sElim SBool _ b = b

-- (SI a) entails (Str a)
class    Str a    where str :: String
instance Str Int  where str = "INT"
instance Str Bool where str = "BOOL"

-- Attach the instance I want to this wrapper, that has the same
-- representation as `a'.
--
-- So I define an instance
--
--   SI a => Str (Wrap a)
-- 
-- and then unsafeCoerce between
--
--   SI a |- Str (Wrap a)
--   SI a |- Str a
-- 
newtype Wrap a = Wrap a

instance SI a => Str (Wrap a) where
  str = sElim (s @a) 
    (str @a) 
    (str @a)

wit :: forall a. SI a |- Str a
wit = wrapElim Dict where

  wrapElim :: (SI a |- Str (Wrap a))
           -> (SI a |- Str a)
  wrapElim = unsafeCoerce

-- >> siStr @Int
-- "INT!"
-- >> siStr @Bool
-- "BOOL!"
siStr :: forall a. SI a => String
siStr = go wit where

  go :: SI a => (SI a |- Str a) -> String
  go Dict = str @a ++ "!"

I claim that SI a |- Str a dictionary describes something like

instance SI a => Str a where
  str :: String
  str = sElim (s @a) (str @a) (str @a)

Where we handle both cases: SI Int (str @a) and SI Bool (str @a). “Can't the user add SI instances that we have no way of handling?”, only with garbage s = undefined because there are only two S a-constructors but they are already defined and handled. The above hack seems to work (and is sensible to boot unless I'm missing something). Is there a problem with this?

Last edited 18 months ago by Iceland_jack (previous) (diff)

comment:4 Changed 18 months ago by Iceland_jack

Using #14292 this can be coerced rather than unsafeCoerced if only we turn on -XIncoherentInstances and mark some parameters representational

type role Implies nominal representational
type role Str representational

comment:5 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.