Opened 4 years ago

Last modified 10 months ago

#11594 new feature request

closed empty type families fully applied get reduced lazily when in a constraint tuple and fully applied

Reported by: carter Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 7.10.2
Keywords: Cc: adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #9636 Differential Rev(s):
Wiki Page:

Description

in an effort to simulate the TypeError close type family in userland, I was doing a bit of experimentation with type families in ghc 7.10 and 8.0 RC2, and i was surprised to find that i can't get fully applied closed type families to reduce "strictly" when they are fully applied to concrete arguments within a Constraint Tuple.

Roughly, I want to be able to write "Assert x" style predicates in a type signature, and have those be checked/ reduced at the definition site rather than the use site. It seems like what I would have to do is do a slight indirection the form

publicFunName :: SimpleType c1 c2 --- c1 c2 are two concrete types 
publicFunName ... = guardedFun
   where 
     guardedFun :: (MyClosedTypeFamAssert c1 c2)=> SimpleType c1 c2
     guardedFun ... = ... 
      -- myClosedTypeFamAssert (x :: *) (y :: *) :: Constraint 

I guess this SORTOF makes sense that it doesn't get reduced strictly at the definition site (though its a sort of normalization i feel like). I think the sibling computation where i have myClosedTypeFamAssert (x :: *) (y :: *) :: Bool and have the guard be ('True ~ myClosedTypeFamAssert c1 c2 ), but I was hoping i could have things look a teeny bit more "Assertion" style for aesthetical reasons

enclosed below is a self contained module that exhibits a more worked out example

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-} 

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeInType, ConstraintKinds #-}

module Main where

import GHC.Types (Constraint,TYPE,Levity(..))

main = print  (7 :: Int)-- this works
-- main = print (sevenBad :: Int ) -- this does error, but its at the use site rather than definition site!


-- using this one ""works"", but results in a VERY confusing type error involving 
-- 
type family WorstClosedStuckError (x :: a) :: Constraint where 
    WorstClosedStuckError a = (False ~ True)


--- empty closed type families are ONLY allowed as of ghc 8.0
type family ClosedStuckSilly (x :: a) :: b  where  
type family ClosedStuckSillyConstr (x :: a) :: Constraint  where 
--- this is analogous to a version of the TypeError family in GHC.TypeLits in 8.0 onwards
--- but kind polymorphic closed empty type families dont seem to trigger a type error in the definition site 
--- but rather in the USE site 

type family  ClosedStuckTypeConstr (x :: TYPE Lifted) :: Constraint where 
type family  ClosedStuckType (x :: TYPE Lifted) :: b where   
  --- these two seem to work OK 

-- these two only only report an error once I resolve the constraint on a to something like Int etc
sevenBad :: (ClosedStuckSilly 'True , Num a) => a 
sevenBad = 7 
sevenOtherBad :: (ClosedStuckSillyConstr 'False, Num a) => a 
sevenOtherBad = 7 

-- this one fails to type check at the definition site, but has a SUPER confusing 
-- error about allow ambiguous types
sevenBadWorst ::  (WorstClosedStuckError 'False, Num a) => a
sevenBadWorst = 7 

sevenOKButNotUseful :: (ClosedStuckType Bool, Num a) => a 
sevenOKButNotUseful = 7 

-- i have to do an indirection to force an "assertion" / "reduction", the following triggers the error as expected
sevenIndirect :: Num a => a
sevenIndirect = sevenBad


Change History (13)

comment:1 Changed 4 years ago by goldfire

I'm a bit lost here. Can you give a small example that exhibits some behavior you disagree with and say what it is that's disagreeable? The range of examples above is helpful, but I'm not sure what's the signal and what's the noise.

comment:2 Changed 4 years ago by carter

the meat of it is i want the folllowing to not type check

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-} 

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeInType, ConstraintKinds #-}

module MyLIbrary(sevenBad) where

import GHC.Types (Constraint,TYPE,Levity(..))

-- these two only only report an error once I 
---resolve the constraint on a to something like Int etc
sevenBad :: (ClosedStuckSilly 'True , Num a) => a 
sevenBad = 7 


type family ClosedStuckSilly (x :: a) :: b  where  

if i instead write something like

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-} 

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeInType, ConstraintKinds #-}

module MyLIbrary(sevenBadWrapped) where

import GHC.Types (Constraint,TYPE,Levity(..))

-- these two only only report an error once I resolve 
---the constraint on a to something like Int etc
sevenBad :: (ClosedStuckSilly 'True , Num a) => a 
sevenBad = 7 

sevenBadWrapped :: Num a => a 
sevenBadWrapped = sevenBad

type family ClosedStuckSilly (x :: a) :: b  where  


i'll get the type error i want, but that, I fear, wont scale very well in terms of usability for more complex codes

comment:3 Changed 4 years ago by goldfire

Type: bugfeature request

To paraphrase, you want GHC to recognize that an empty closed type family is insoluble.

Although this is a decent suggestion, would a use of TypeError work for you?

comment:4 Changed 4 years ago by carter

I guess it could be viewed as a feature request.

I need to play around with the 8.0 / master a bit to have a clear sense of if TypeError alone suffices, but I DO think that from a user / usability perspective, the fact that we DO present the definition of TypeError as being an empty closed type family in GHC.TypeLits will be confusing for some users.

I think either

a) the documentation in http://downloads.haskell.org/~ghc/8.0.1-rc2/docs/html/libraries/base-4.9.0.0/GHC-TypeLits.html#g:4 (the GHC.TypeLits module) should be changed to clearly articulate that TypeError has special wired-in behavior that can't be replicated in userland, (including what special treatment it gets versus userland type families that are written simularly) OR

b) anything that has a reasonable looking source definition in base that isn't the infinite loop style found in http://downloads.haskell.org/~ghc/8.0.1-rc2/docs/html/libraries/ghc-prim-0.5.0.0/GHC-Prim.html and not explicitly documented as being a deeply magical / wired-in behavior really should be replicable in userland

zooming out: its probably the case that for me, TypeError will probably be fine for me, but my main concern is about having a clearer understanding of whats a magical special case and what isnt', and how the semantics of the pieces of magics is clearly articulated

comment:5 in reply to:  3 ; Changed 4 years ago by adamgundry

Cc: adamgundry added

Replying to goldfire:

To paraphrase, you want GHC to recognize that an empty closed type family is insoluble.

Note that empty closed type families are not necessarily insoluble in the presence of type-checker plugins. Indeed, the whole point of adding empty CTFs was to allow them to be given special reduction behaviour by plugins. So I think the implementation should be left alone (but for some contrasting views see the discussion on #9636).

Documentation improvements are welcome, of course. :-)

comment:6 in reply to:  5 ; Changed 4 years ago by carter

So if I wanted a new userland insolvable type family that errors out eagerly rather than down stream, I'd have to have a type solver plugin active in the defining module to enforce that?

I guess that would enable simulating the type error family in userland In 7.10 right? I guess my main worry is that afaict, any type solver plugin usage forces ghc to rebuild The offending module every time. And then every down stream user possibly too!

Or am I mis understanding your point?

What if instead, when defining an empty closed type family, we could pragma Annotate it with "requires plugin foo" when we want this other plugin adhuncated semantics, Because otherwise requiring the offending type plugin is implicit in any down stream module!

Replying to adamgundry:

Replying to goldfire:

To paraphrase, you want GHC to recognize that an empty closed type family is insoluble.

Note that empty closed type families are not necessarily insoluble in the presence of type-checker plugins. Indeed, the whole point of adding empty CTFs was to allow them to be given special reduction behaviour by plugins. So I think the implementation should be left alone (but for some contrasting views see the discussion on #9636).

Documentation improvements are welcome, of course. :-)

comment:7 Changed 4 years ago by goldfire

I think option (a) from comment:4 is the best way forward here: document TypeError more carefully. I will say that the feature is described in the manual in the section entitled Custom compile-time errors.

comment:8 in reply to:  6 Changed 4 years ago by adamgundry

Replying to carter:

So if I wanted a new userland insolvable type family that errors out eagerly rather than down stream, I'd have to have a type solver plugin active in the defining module to enforce that?

I guess that would enable simulating the type error family in userland In 7.10 right?

The plugin would need to be active at use sites, not definition sites, but yes - it is possible for plugins to approximately simulate TypeError. They can't give exactly the same semantics, because plugins only get to see unsolved constraints, but can work the same way for uses of TypeError at kind Constraint.

In fact I hacked together a quick prototype plugin that does exactly that during the last ICFP. If there's interest, I'm happy to share the code, though it's not entirely consistent with the TypeError API.

What if instead, when defining an empty closed type family, we could pragma Annotate it with "requires plugin foo" when we want this other plugin adhuncated semantics, Because otherwise requiring the offending type plugin is implicit in any down stream module!

Right, there is currently no way to indicate which type-checker plugins a module requires, and it might be nice to do so.

comment:9 Changed 4 years ago by thoughtpolice

Milestone: 8.0.18.2.1

Punting to 8.2.1, since it seems any real 'fix' will require a bit of design work (and in the mean time, from a quick skim, it seems TypeError is fine here.)

comment:10 Changed 3 years ago by rwbarton

Milestone: 8.2.18.4.1

comment:11 Changed 21 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:12 Changed 16 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for 8.6, bumping to 8.8.

comment:13 Changed 10 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.