[GHC] #11594: closed empty type families fully applied get reduced lazily when in a constraint tuple and fully applied

[GHC]

#11594: closed empty type families  fully applied get reduced lazily when in a
constraint tuple and fully applied
-------------------------------------+-------------------------------------
           Reporter:  carter         |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.0.1
          Component:  Compiler       |           Version:  7.10.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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


 }}}

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