closed empty type families fully applied get reduced lazily when in a constraint tuple and fully applied
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
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |